let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G holds
( H,N are_complements_in G iff ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G ) )
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G holds
( H,N are_complements_in G iff ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G ) )
let N be normal Subgroup of G; :: thesis: ( H,N are_complements_in G iff ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G ) )
the carrier of G c= the carrier of G ;
then reconsider A = the carrier of G as Subset of G ;
thus ( H,N are_complements_in G implies ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G ) ) :: thesis: ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G implies H,N are_complements_in G )

proof

assume A1: H,N are_complements_in G ; :: thesis: ( H "\/" N = multMagma(# the carrier of G, the multF of G #) & H /\ N = (1). G )
then H "\/" N = gr A by GROUP_4:50;
hence H "\/" N = multMagma(# the carrier of G, the multF of G #) by Th48; :: thesis: H /\ N = (1). G
thus H /\ N = (1). G by A1; :: thesis: verum

end;

assume A1: H "\/" N = multMagma(# the carrier of G, the multF of G #) ; :: thesis: ( not H /\ N = (1). G or H,N are_complements_in G )
A2: H * N = (carr H) * N by GROUP_4:43
.= N * (carr H) by GROUP_3:120
.= N * H by GROUP_4:43 ;
assume H /\ N = (1). G ; :: thesis: H,N are_complements_in G
hence H,N are_complements_in G by A1, A2, GROUP_4:51; :: thesis: verum