let G be Group; :: thesis: for A being non empty Subset of G
for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )
let A be non empty Subset of G; :: thesis: for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )
let N1, N2 be strict normal Subgroup of G; :: thesis: ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )
consider N being strict normal Subgroup of G such that
A1: the carrier of N = N1 * N2 by Th8;
( N1 is Subgroup of N & N2 is Subgroup of N ) by A1, Th9;
then A2: ( N ` A c= N1 ` A & N ` A c= N2 ` A ) by Th25;
N ` A c= (N1 ` A) /\ (N2 ` A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N ` A or x in (N1 ` A) /\ (N2 ` A) )
assume x in N ` A ; :: thesis: x in (N1 ` A) /\ (N2 ` A)
hence x in (N1 ` A) /\ (N2 ` A) by A2, XBOOLE_0:def 4; :: thesis: verum

end;

hence ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) ) by A1; :: thesis: verum