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