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