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
G ./. N,H are_isomorphic
let H be Subgroup of G; :: thesis: for N being normal Subgroup of G st H,N are_complements_in G holds
G ./. N,H are_isomorphic
let N be normal Subgroup of G; :: thesis: ( H,N are_complements_in G implies G ./. N,H are_isomorphic )
assume H,N are_complements_in G ; :: thesis: G ./. N,H are_isomorphic
then ex phi being Homomorphism of H,(G ./. N) st
( ( for h being Element of H
for g being Element of G st g = h holds
phi . h = g * N ) & phi is bijective ) by Th55;
hence G ./. N,H are_isomorphic by GROUP_6:def 11; :: thesis: verum