let G be Group; :: thesis: for I being non empty set
for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)
let I be non empty set ; :: thesis: for F being componentwise_strict Subgroup-Family of I,G
for Fam being Subset of (Subgroups G) st Fam = rng F holds
union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)
let F be componentwise_strict Subgroup-Family of I,G; :: thesis: for Fam being Subset of (Subgroups G) st Fam = rng F holds
union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)
let Fam be Subset of (Subgroups G); :: thesis: ( Fam = rng F implies union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F) )
assume A1: Fam = rng F ; :: thesis: union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F)
set X = { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } ;
for x being object holds
( x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } iff x in rng (Carrier F) )

proof

let x be object ; :: thesis: ( x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } iff x in rng (Carrier F) )

hereby :: thesis: ( x in rng (Carrier F) implies x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } )

assume x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } ; :: thesis: x in rng (Carrier F)
then consider A being Subset of G such that
A2: ( x = A & ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) ) ;
consider H being strict Subgroup of G such that
A3: ( H in Fam & x = the carrier of H ) by A2;
consider i being Element of I such that
A4: H = F . i by A1, A3, MssRng;
x = (Carrier F) . i by A3, A4, Th9;
hence x in rng (Carrier F) by MssRng; :: thesis: verum

end;

assume x in rng (Carrier F) ; :: thesis: x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) }
then consider i being Element of I such that
A5: x = (Carrier F) . i by MssRng;
F . i is strict Subgroup of G by Def19;
then consider H being strict Subgroup of G such that
A6: H = F . i ;
A8: H in Fam by A1, A6, MssRng;
ex A being Subset of G st
( x = A & ex H0 being strict Subgroup of G st
( A = the carrier of H0 & H0 in Fam ) )

proof

take A = carr H; :: thesis: ( x = A & ex H0 being strict Subgroup of G st
( A = the carrier of H0 & H0 in Fam ) )
thus ( x = A & ex H0 being strict Subgroup of G st
( A = the carrier of H0 & H0 in Fam ) ) by A8, A5, A6, Th9; :: thesis: verum

end;

hence x in { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } ; :: thesis: verum

end;

then { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = rng (Carrier F) by TARSKI:2;
hence union { A where A is Subset of G : ex H being strict Subgroup of G st
( H in Fam & A = the carrier of H ) } = Union (Carrier F) by CARD_3:def 4; :: thesis: verum