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