let G be addGroup; :: thesis: for f, g, h being Element of G holds
( f + h = g iff f = g + (- h) )
let f, g, h be Element of G; :: thesis: ( f + h = g iff f = g + (- h) )
(g + (- h)) + h = g + ((- h) + h) by RLVECT_1:def 3
.= g + (0_ G) by Def5
.= g by Def4 ;
hence ( f + h = g implies f = g + (- h) ) by Th6; :: thesis: ( f = g + (- h) implies f + h = g )
assume f = g + (- h) ; :: thesis: f + h = g
hence f + h = g + ((- h) + h) by RLVECT_1:def 3
.= g + (0_ G) by Def5
.= g by Def4 ;
:: thesis: verum