let h be Form of V,W; :: thesis: ( h = f - g iff for v being Vector of V
for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w) )
thus ( h = f - g implies for v being Vector of V
for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w) ) :: thesis: ( ( for v being Vector of V
for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w) ) implies h = f - g )

proof

assume A1: h = f - g ; :: thesis: for v being Vector of V
for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w)
let v be Vector of V; :: thesis: for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w)
let w be Vector of W; :: thesis: h . v,w = (f . v,w) - (g . v,w)
thus h . v,w = (f . v,w) + ((- g) . v,w) by A1, Def3
.= (f . v,w) + (- (g . v,w)) by Def5
.= (f . v,w) - (g . v,w) by RLVECT_1:def 12 ; :: thesis: verum

end;

assume A2: for v being Vector of V
for w being Vector of W holds h . v,w = (f . v,w) - (g . v,w) ; :: thesis: h = f - g

now

let v be Vector of V; :: thesis: for w being Vector of W holds h . v,w = (f - g) . v,w
let w be Vector of W; :: thesis: h . v,w = (f - g) . v,w
thus h . v,w = (f . v,w) - (g . v,w) by A2
.= (f . v,w) + (- (g . v,w)) by RLVECT_1:def 12
.= (f . v,w) + ((- g) . v,w) by Def5
.= (f - g) . v,w by Def3 ; :: thesis: verum

end;

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