let G be Group; :: thesis: for I being set
for J being 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 I be set ; :: thesis: for J being 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 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

per cases ( J is empty or not J is empty ) ;

suppose J is empty ; :: thesis: ex N being strict normal Subgroup of G st N = gr A

then Carrier (F | J) = {} --> (bool the carrier of G) ;
then Union (Carrier (F | J)) = {} by FUNCT_6:26;
then A2: A = {} the carrier of G by A1, SUBSET_1:def 2;
take N = (1). G; :: thesis: N = gr A
thus N = gr A by A2, GROUP_4:30; :: thesis: verum

end;

suppose A3: not J is empty ; :: thesis: ex N being strict normal Subgroup of G st N = gr A

then ex x being object st x in J by XBOOLE_0:def 1;
then reconsider I = I as non empty set ;
reconsider J = J as non empty Subset of I by A3;
reconsider F = F as normal Subgroup-Family of I,G ;
A = Union (Carrier (F | J)) by A1;
hence ex N being strict normal Subgroup of G st N = gr A by LmJoinNormUnionRes; :: thesis: verum

end;

end;