let G be Group; :: thesis: for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds
( N1 is Subgroup of N & N2 is Subgroup of N )
let N, N1, N2 be Subgroup of G; :: thesis: ( the carrier of N = N1 * N2 implies ( N1 is Subgroup of N & N2 is Subgroup of N ) )
assume A1: the carrier of N = N1 * N2 ; :: thesis: ( N1 is Subgroup of N & N2 is Subgroup of N )
for x being Element of G st x in N1 holds
x in N

proof

let x be Element of G; :: thesis: ( x in N1 implies x in N )
assume A2: x in N1 ; :: thesis: x in N
A3: 1_ G in N2 by GROUP_2:46;
x = x * (1_ G) by GROUP_1:def 4;
then x in N1 * N2 by A2, A3, Th6;
hence x in N by A1, STRUCT_0:def 5; :: thesis: verum

end;

hence N1 is Subgroup of N by GROUP_2:58; :: thesis: N2 is Subgroup of N
for y being Element of G st y in N2 holds
y in N

proof

let y be Element of G; :: thesis: ( y in N2 implies y in N )
assume A4: y in N2 ; :: thesis: y in N
A5: 1_ G in N1 by GROUP_2:46;
y = (1_ G) * y by GROUP_1:def 4;
then y in N1 * N2 by A4, A5, Th6;
hence y in N by A1, STRUCT_0:def 5; :: thesis: verum

end;

hence N2 is Subgroup of N by GROUP_2:58; :: thesis: verum