let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for x, y being Element of R ex z being Element of R st
( x = y + z & x = z + y )
let x, y be Element of R; :: thesis: ex z being Element of R st
( x = y + z & x = z + y )
take z = (- y) + x; :: thesis: ( x = y + z & x = z + y )
z + y = x + ((- y) + y) by RLVECT_1:def 3
.= x + (0. R) by RLVECT_1:5
.= x by RLVECT_1:4 ;
hence ( x = y + z & x = z + y ) ; :: thesis: verum