let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for x, z, y being Scalar of R st x = z - y holds
x + y = z
let x, z, y be Scalar of R; :: thesis: ( x = z - y implies x + y = z )
assume x = z - y ; :: thesis: x + y = z
then x + y = z + (y + (- y)) by RLVECT_1:def 3
.= z + (0. R) by RLVECT_1:def 10
.= z by RLVECT_1:4 ;
hence x + y = z ; :: thesis: verum