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:17;
hence ( - a = 0. F implies a = 0. F ) by RLVECT_1:12; :: thesis: verum