let I be non empty set ; :: thesis: for G being Group
for J being non empty Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A
let G be Group; :: thesis: for J being non empty Subset of I
for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A
let J be non empty Subset of I; :: thesis: for F being normal Subgroup-Family of I,G
for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A
let F be normal Subgroup-Family of I,G; :: thesis: for A being Subset of G st A = Union (Carrier (F | J)) holds
ex N being strict normal Subgroup of G st N = gr A
let A be Subset of G; :: thesis: ( A = Union (Carrier (F | J)) implies ex N being strict normal Subgroup of G st N = gr A )
assume A1: A = Union (Carrier (F | J)) ; :: thesis: ex N being strict normal Subgroup of G st N = gr A
set Fam = { the carrier of ((F | J) . j) where j is Element of J : verum } ;
set X = union { the carrier of ((F | J) . j) where j is Element of J : verum } ;
for x being object holds
( x in A iff x in union { the carrier of ((F | J) . j) where j is Element of J : verum } )

proof

let x be object ; :: thesis: ( x in A iff x in union { the carrier of ((F | J) . j) where j is Element of J : verum } )

hereby :: thesis: ( x in union { the carrier of ((F | J) . j) where j is Element of J : verum } implies x in A )

assume x in A ; :: thesis: x in union { the carrier of ((F | J) . j) where j is Element of J : verum }
then x in union (rng (Carrier (F | J))) by A1, CARD_3:def 4;
then consider Uj being set such that
B1: ( x in Uj & Uj in rng (Carrier (F | J)) ) by TARSKI:def 4;
consider j being Element of J such that
B2: Uj = (Carrier (F | J)) . j by B1, MssRng;
Uj = the carrier of ((F | J) . j) by B2, Th9;
then Uj in { the carrier of ((F | J) . j) where j is Element of J : verum } ;
hence x in union { the carrier of ((F | J) . j) where j is Element of J : verum } by B1, TARSKI:def 4; :: thesis: verum

end;

assume x in union { the carrier of ((F | J) . j) where j is Element of J : verum } ; :: thesis: x in A
then consider Uj being set such that
B3: ( x in Uj & Uj in { the carrier of ((F | J) . j) where j is Element of J : verum } ) by TARSKI:def 4;
consider j being Element of J such that
B4: Uj = the carrier of ((F | J) . j) by B3;
B5: dom (Carrier (F | J)) = J by PARTFUN1:def 2;
Uj = (Carrier (F | J)) . j by B4, Th9;
then Uj in rng (Carrier (F | J)) by B5, FUNCT_1:3;
then x in union (rng (Carrier (F | J))) by B3, TARSKI:def 4;
hence x in A by A1, CARD_3:def 4; :: thesis: verum

end;

hence ex N being strict normal Subgroup of G st N = gr A by ThJoinNorm, TARSKI:2; :: thesis: verum