let F, G be Form of V,W; ( ( for v being Vector of V
for w being Vector of W holds F . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds G . (v,w) = a * (f . (v,w)) ) implies F = G )
assume that
A2:
for v being Vector of V
for w being Vector of W holds F . (v,w) = a * (f . (v,w))
and
A3:
for v being Vector of V
for w being Vector of W holds G . (v,w) = a * (f . (v,w))
; F = G
now for v being Vector of V
for w being Vector of W holds F . (v,w) = G . (v,w)let v be
Vector of
V;
for w being Vector of W holds F . (v,w) = G . (v,w)let w be
Vector of
W;
F . (v,w) = G . (v,w)thus F . (
v,
w) =
a * (f . (v,w))
by A2
.=
G . (
v,
w)
by A3
;
verum end;
hence
F = G
; verum