let G be addGroup; :: 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: addMagma(# the carrier of H1, the addF of H1 #) = H2 * g ; :: according to GROUP_1A:def 39 :: thesis: ex g being Element of G st H2 = H1 * g
H1 * (- g) = H2 by A1, ThB62;
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, ThB62;
hence H1,H2 are_conjugated ; :: thesis: verum