let G be Group; :: thesis: for H1, H2 being Subgroup of G
for N being normal Subgroup of G st H1,N are_complements_in G & H2,N are_complements_in G holds
H1,H2 are_isomorphic
let H1, H2 be Subgroup of G; :: thesis: for N being normal Subgroup of G st H1,N are_complements_in G & H2,N are_complements_in G holds
H1,H2 are_isomorphic
let N be normal Subgroup of G; :: thesis: ( H1,N are_complements_in G & H2,N are_complements_in G implies H1,H2 are_isomorphic )
assume H1,N are_complements_in G ; :: thesis: ( not H2,N are_complements_in G or H1,H2 are_isomorphic )
then A3: G ./. N,H1 are_isomorphic by Th56;
assume H2,N are_complements_in G ; :: thesis: H1,H2 are_isomorphic
then G ./. N,H2 are_isomorphic by Th56;
hence H1,H2 are_isomorphic by A3, GROUP_6:67; :: thesis: verum