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