let G be addGroup; :: thesis: for a being Element of G holds
( ((0). G) + a = {a} & a + ((0). G) = {a} )
let a be Element of G; :: thesis: ( ((0). G) + a = {a} & a + ((0). G) = {a} )
A1: the carrier of ((0). G) = {(0_ G)} by Def7;
hence ((0). G) + a = {((0_ G) + a)} by Th18
.= {a} by Def4 ;
:: thesis: a + ((0). G) = {a}
thus a + ((0). G) = {(a + (0_ G))} by A1, Th18
.= {a} by Def4 ; :: thesis: verum