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