let h1, h2 be Element of G; :: thesis: ( h + h1 = 0_ G & h1 + h = 0_ G & h + h2 = 0_ G & h2 + h = 0_ G implies h1 = h2 )
assume that
A3: h + h1 = 0_ G and
h1 + h = 0_ G and
h + h2 = 0_ G and
A4: h2 + h = 0_ G ; :: thesis: h1 = h2
thus h1 = (0_ G) + h1 by Def4
.= h2 + (h + h1) by A4, RLVECT_1:def 3
.= h2 by A3, Def4 ; :: thesis: verum