let G be addGroup; :: thesis: for A being Subset of G holds A * (0_ G) = A
let A be Subset of G; :: thesis: A * (0_ G) = A
thus A * (0_ G) = ((- (0_ G)) + A) + (0_ G) by Th50
.= (- (0_ G)) + A by Th37
.= (0_ G) + A by Th8
.= A by Th37 ; :: thesis: verum