let F be Field; :: thesis: for a being non zero Element of F holds - ((- a) ") = a "
let a be non zero Element of F; :: thesis: - ((- a) ") = a "
(a ") - (- ((- a) ")) = (a ") + (- (a ")) by XZ
.= 0. F by RLVECT_1:5 ;
hence - ((- a) ") = a " by RLVECT_1:21; :: thesis: verum