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

proof

given g being Element of G such that A1: a = b |^ g ; :: according to GROUP_3:def 7 :: thesis: ex g being Element of G st b = a |^ g
a |^ (g " ) = b by A1, Th30;
hence ex g being Element of G st b = a |^ g ; :: thesis: verum

end;

given g being Element of G such that A2: b = a |^ g ; :: thesis: a,b are_conjugated
a = b |^ (g " ) by A2, Th30;
hence a,b are_conjugated by Def7; :: thesis: verum