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

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