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

proof

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

now :: thesis: for v being Vector of V
for w being Vector of W holds g . (v,w) = ((- (1. F_Real)) * f) . (v,w)

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

end;

hence g = (- (1. F_Real)) * f ; :: thesis: verum

end;

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

now :: thesis: for v being Vector of V
for w being Vector of W holds g . (v,w) = (- f) . (v,w)

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. F_Real)) * (f . (v,w)) by A2, Def3
.= - (f . (v,w))
.= (- f) . (v,w) by Def4 ; :: thesis: verum

end;

hence g = - f ; :: thesis: verum