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
X: ( not a " is zero & not - (a ") is zero ) by VECTSP_1:25;
(- ((a ") ")) * (- (a ")) = ((a ") ") * (a ") by VECTSP_1:10
.= 1_ F by X, VECTSP_2:9 ;
hence (- (a ")) " = - a by VECTSP_2:10; :: thesis: verum