let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of F st a - b = 0. F holds
a = b
let a, b be Element of F; :: thesis: ( a - b = 0. F implies a = b )
assume a - b = 0. F ; :: thesis: a = b
then a + (- b) = 0. F by RLVECT_1:def 11;
then a = - (- b) by RLVECT_1:6;
hence a = b by RLVECT_1:17; :: thesis: verum