let G be addGroup; :: thesis: for a being Element of G st ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) holds
a = 0_ G
let a be Element of G; :: thesis: ( ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) implies a = 0_ G )
assume A1: ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) ; :: thesis: a = 0_ G

now :: thesis: a = 0_ G

per cases ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) by A1;

suppose a, 0_ G are_conjugated ; :: thesis: a = 0_ G

then ex g being Element of G st 0_ G = a * g by Th74;
hence a = 0_ G by ThB18; :: thesis: verum

end;

suppose 0_ G,a are_conjugated ; :: thesis: a = 0_ G

hence a = 0_ G by ThB18; :: thesis: verum

end;

end;

end;

hence a = 0_ G ; :: thesis: verum