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 ) )
A1: ( 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;
A2: ( 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 11;
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;
( x = y implies x - y = 0. F )
proof
assume x = y ; :: thesis: x - y = 0. F
then x - y = y + (- y) by RLVECT_1:def 11;
hence x - y = 0. F by RLVECT_1:5; :: 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 A1, A2, RLVECT_1:5; :: thesis: verum