let F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a being Element of F st - a = 0. F holds
a = 0. F
let a be Element of F; :: thesis: ( - a = 0. F implies a = 0. F )
- (- a) = a by RLVECT_1:30;
hence ( - a = 0. F implies a = 0. F ) by RLVECT_1:25; :: thesis: verum