:: deftheorem defines is_internal_product_of GROUP_23:def 24 :
for G being Group
for Fam being Subset of (Subgroups G) holds
( G is_internal_product_of Fam iff ( ( for H being strict Subgroup of G st H in Fam holds
H is normal Subgroup of G ) & ex A being Subset of G st
( A = union { UH where UH is Subset of G : ex H being strict Subgroup of G st
( H in Fam & UH = the carrier of H ) } & multMagma(# the carrier of G, the multF of G #) = gr A ) & ( for H being strict Subgroup of G st H in Fam holds
for A being Subset of G st A = union { UK where UK is Subset of G : ex K being strict Subgroup of G st
( K in Fam & UK = the carrier of K & K <> H ) } holds
H /\ (gr A) = (1). G ) ) );