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