let p be Prime; :: thesis: for G being finite Group
for N1, N2 being normal Subgroup of G st N1 is p -group & N2 is p -group holds
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -group )
let G be finite Group; :: thesis: for N1, N2 being normal Subgroup of G st N1 is p -group & N2 is p -group holds
ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -group )
let N1, N2 be normal Subgroup of G; :: thesis: ( N1 is p -group & N2 is p -group implies ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -group ) )
assume ( N1 is p -group & N2 is p -group ) ; :: thesis: ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -group )
then consider N being strict Subgroup of G such that
A1: ( the carrier of N = N1 * N2 & N is p -group ) by Th20;
for x, y being Element of G st y in N holds
(x * y) * (x ") in N

proof

let x, y be Element of G; :: thesis: ( y in N implies (x * y) * (x ") in N )
assume y in N ; :: thesis: (x * y) * (x ") in N
then y in the carrier of N ;
then consider a, b being Element of G such that
A2: ( y = a * b & a in N1 & b in N2 ) by A1, GROUP_11:6;
A3: (x * y) * (x ") = ((x * a) * b) * (x ") by A2, GROUP_1:def 3
.= (x * a) * (b * (x ")) by GROUP_1:def 3
.= ((x * a) * (1_ G)) * (b * (x ")) by GROUP_1:def 4
.= ((x * a) * ((x ") * x)) * (b * (x ")) by GROUP_1:def 5
.= (((x * a) * (x ")) * x) * (b * (x ")) by GROUP_1:def 3
.= ((x * a) * (x ")) * (x * (b * (x "))) by GROUP_1:def 3
.= ((x * a) * (x ")) * ((x * b) * (x ")) by GROUP_1:def 3 ;
( (x * a) * (x ") in N1 & (x * b) * (x ") in N2 ) by A2, GROUP_11:4;
then (x * y) * (x ") in N1 * N2 by A3, GROUP_11:6;
hence (x * y) * (x ") in N by A1; :: thesis: verum

end;

then N is normal Subgroup of G by GROUP_11:5;
hence ex N being strict normal Subgroup of G st
( the carrier of N = N1 * N2 & N is p -group ) by A1; :: thesis: verum