let G be Group; :: thesis: for H being Subgroup of G
for N being normal Subgroup of G st H,N are_complements_in G holds
( H * N = the carrier of G & N * H = the carrier of G )
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G st H,N are_complements_in G holds
( H * N = the carrier of G & N * H = the carrier of G )
let N be normal Subgroup of G; :: thesis: ( H,N are_complements_in G implies ( H * N = the carrier of G & N * H = the carrier of G ) )
assume A1: H,N are_complements_in G ; :: thesis: ( H * N = the carrier of G & N * H = the carrier of G )
then H "\/" N = multMagma(# the carrier of G, the multF of G #) by Th49;
hence ( H * N = the carrier of G & N * H = the carrier of G ) by A1, Th63; :: thesis: verum