let p be prime Nat; :: thesis:
let G be finite Group; :: thesis:
let N1, N2 be normal Subgroup of G; :: thesis:
assume ( N1 is p -group & N2 is p -group ) ; :: thesis:
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

let x, y be Element of G; :: thesis:
assume y in N ; :: thesis:
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:

end;