let G be addGroup; :: thesis: for a being Element of G holds a,a are_conjugated
let a be Element of G; :: thesis: a,a are_conjugated
take 0_ G ; :: according to GROUP_1A:def 35 :: thesis: a = a * (0_ G)
thus a = a * (0_ G) by Th19; :: thesis: verum