let G be addGroup; :: 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_1A:def 35 :: thesis: ex g being Element of G st b = a * g
a * (- g) = b by A1, ThB25;
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, ThB25;
hence a,b are_conjugated ; :: thesis: verum