[STATEMENT]
lemma direct_decompD:
  assumes "direct_decomp A ss"
  shows "qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A" and "inj_on sum_list (listset ss)"
    and "sum_list ` listset ss = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A) &&& inj_on sum_list (listset ss) &&& sum_list ` listset ss = A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
direct_decomp A ss

goal (1 subgoal):
 1. (qs \<in> listset ss \<Longrightarrow> sum_list qs \<in> A) &&& inj_on sum_list (listset ss) &&& sum_list ` listset ss = A
[PROOF STEP]
by (auto simp: direct_decomp_def bij_betw_def)