let G be addGroup; :: thesis: for a being Element of G holds a * a = a
let a be Element of G; :: thesis: a * a = a
thus a * a = (0_ G) + a by Def5
.= a by Def4 ; :: thesis: verum