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
A1: the carrier of ((0). G) = {(0_ G)} by Def7;
the carrier of (((0). G) * a) = (carr ((0). G)) * a by Def6A
.= {((0_ G) * a)} by A1, ThB37
.= {(0_ G)} by Th17 ;
hence ((0). G) * a = (0). G by Def7; :: thesis: verum