let G be addGroup; :: thesis:
let a be Element of G; :: thesis:
assume A1: ( a, 0_ G are_conjugated or 0_ G,a are_conjugated ) ; :: thesis:

now :: thesis:

per cases by A1;

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

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

end;

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

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

end;

end;

end;

hence a = 0_ G ; :: thesis: