theorem Th49: :: GROUP_24:52

for G being Group
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 ) )