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

for y being Element of G st y in N2 holds

y in N

( 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

hence
N1 is Subgroup of N
by GROUP_2:58; :: thesis: N2 is Subgroup of N
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;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

for y being Element of G st y in N2 holds

y in N

proof

hence
N2 is Subgroup of N
by GROUP_2:58; :: thesis: verum
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;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