thus ( H,N are_complements_in G implies ( N is normal & H * N = the carrier of G & H /\ N = (1). G ) ) :: thesis: ( N is normal & H * N = the carrier of G & H /\ N = (1). G implies H,N are_complements_in G )

proof

assume H,N are_complements_in G ; :: thesis: ( N is normal & H * N = the carrier of G & H /\ N = (1). G )
then consider H1 being strict Subgroup of G, N1 being strict normal Subgroup of G such that
A1: ( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G ) ;
for g being Element of G holds N |^ g = multMagma(# the carrier of N, the multF of N #)

proof

let g be Element of G; :: thesis: N |^ g = multMagma(# the carrier of N, the multF of N #)
B1: carr N1 = carr N by A1;
the carrier of (N |^ g) = (carr N) |^ g by GROUP_3:def 6
.= the carrier of (N1 |^ g) by B1, GROUP_3:def 6
.= the carrier of N1 by GROUP_3:def 13
.= the carrier of N by B1 ;
hence N |^ g = multMagma(# the carrier of N, the multF of N #) by GROUP_2:59; :: thesis: verum

end;

hence N is normal by GROUP_3:def 13; :: thesis: ( H * N = the carrier of G & H /\ N = (1). G )
thus H * N = the carrier of G by A1, Th42; :: thesis: H /\ N = (1). G
thus H /\ N = (1). G by A1, Th42; :: thesis: verum

end;

assume A1: N is normal ; :: thesis: ( not H * N = the carrier of G or not H /\ N = (1). G or H,N are_complements_in G )
assume A2: H * N = the carrier of G ; :: thesis: ( not H /\ N = (1). G or H,N are_complements_in G )
assume A3: H /\ N = (1). G ; :: thesis: H,N are_complements_in G
ex H1 being strict Subgroup of G ex N1 being strict normal Subgroup of G st
( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G )

proof

reconsider H1 = multMagma(# the carrier of H, the multF of H #) as strict Subgroup of G by Th1;
take H1 ; :: thesis: ex N1 being strict normal Subgroup of G st
( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G )
reconsider N1 = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by A1, Th2;
take N1 ; :: thesis: ( H1 = multMagma(# the carrier of H, the multF of H #) & N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G )
thus H1 = multMagma(# the carrier of H, the multF of H #) ; :: thesis: ( N1 = multMagma(# the carrier of N, the multF of N #) & H1 * N1 = the carrier of G & H1 /\ N1 = (1). G )
thus N1 = multMagma(# the carrier of N, the multF of N #) ; :: thesis: ( H1 * N1 = the carrier of G & H1 /\ N1 = (1). G )
thus H1 * N1 = the carrier of G by A2, Th42; :: thesis: H1 /\ N1 = (1). G
thus H1 /\ N1 = (1). G by A3, Th42; :: thesis: verum

end;

hence H,N are_complements_in G ; :: thesis: verum