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 )

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

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 A2:
for v being Vector of V
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, Def2

.= (f . (v,w)) + (- (g . (v,w))) by Def4

.= (f . (v,w)) - (g . (v,w)) by RLVECT_1:def 11 ; :: thesis: verum

end;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, Def2

.= (f . (v,w)) + (- (g . (v,w))) by Def4

.= (f . (v,w)) - (g . (v,w)) by RLVECT_1:def 11 ; :: thesis: verum

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

now :: thesis: for v being Vector of V

for w being Vector of W holds h . (v,w) = (f - g) . (v,w)

hence
h = f - g
; :: thesis: verumfor w being Vector of W holds h . (v,w) = (f - g) . (v,w)

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 11

.= (f . (v,w)) + ((- g) . (v,w)) by Def4

.= (f - g) . (v,w) by Def2 ; :: thesis: verum

end;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 11

.= (f . (v,w)) + ((- g) . (v,w)) by Def4

.= (f - g) . (v,w) by Def2 ; :: thesis: verum