let g be Form of V,W; :: thesis: ( g = - f iff g = (- (1. K)) * f )
thus ( g = - f implies g = (- (1. K)) * f ) :: thesis: ( g = (- (1. K)) * f implies g = - f )

proof

assume A1: g = - f ; :: thesis: g = (- (1. K)) * f

now

let v be Vector of V; :: thesis: for w being Vector of W holds g . v,w = ((- (1. K)) * f) . v,w
let w be Vector of W; :: thesis: g . v,w = ((- (1. K)) * f) . v,w
thus g . v,w = - (f . v,w) by A1, Def5
.= (- (1. K)) * (f . v,w) by VECTSP_2:87
.= ((- (1. K)) * f) . v,w by Def4 ; :: thesis: verum

end;

hence g = (- (1. K)) * f by BINOP_1:2; :: thesis: verum

end;

assume A2: g = (- (1. K)) * f ; :: thesis: g = - f

now

let v be Vector of V; :: thesis: for w being Vector of W holds g . v,w = (- f) . v,w
let w be Vector of W; :: thesis: g . v,w = (- f) . v,w
thus g . v,w = (- (1. K)) * (f . v,w) by A2, Def4
.= - (f . v,w) by VECTSP_2:87
.= (- f) . v,w by Def5 ; :: thesis: verum

end;

hence g = - f by BINOP_1:2; :: thesis: verum