let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x, y being Element of F holds
( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
let x, y be Element of F; :: thesis: ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) )
( x + (- y) = 0. F implies x = y )
proof
assume x + (- y) = 0. F ; :: thesis: x = y
then x + ((- y) + y) = (0. F) + y by RLVECT_1:def 3;
then x + (0. F) = (0. F) + y by RLVECT_1:5;
then x = (0. F) + y by RLVECT_1:4;
hence x = y by RLVECT_1:4; :: thesis: verum
end;
hence ( ( x + (- y) = 0. F implies x = y ) & ( x = y implies x + (- y) = 0. F ) & ( x - y = 0. F implies x = y ) & ( x = y implies x - y = 0. F ) ) by RLVECT_1:5; :: thesis: verum