let G be Group; :: thesis: for H1, H2 being strict Subgroup of G holds
( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
let H1, H2 be strict Subgroup of G; :: thesis: ( H1,H2 are_conjugated iff ex g being Element of G st H2 = H1 |^ g )
thus ( H1,H2 are_conjugated implies ex g being Element of G st H2 = H1 |^ g ) :: thesis: ( ex g being Element of G st H2 = H1 |^ g implies H1,H2 are_conjugated )

proof

given g being Element of G such that A1: multMagma(# the carrier of H1, the multF of H1 #) = H2 |^ g ; :: according to GROUP_3:def 11 :: thesis: ex g being Element of G st H2 = H1 |^ g
H1 |^ (g ") = H2 by A1, Th74;
hence ex g being Element of G st H2 = H1 |^ g ; :: thesis: verum

end;

given g being Element of G such that A2: H2 = H1 |^ g ; :: thesis: H1,H2 are_conjugated
H1 = H2 |^ (g ") by A2, Th74;
hence H1,H2 are_conjugated by Def11; :: thesis: verum