set fg = FormFunctional (f,g);
consider v being Vector of V such that
v <> 0. V
and
A1:
f . v <> 0. K
by VECTSP10:28;
consider w being Vector of W such that
w <> 0. W
and
A2:
g . w <> 0. K
by VECTSP10:28;
(FormFunctional (f,g)) . (v,w) = (f . v) * (g . w)
by Def10;
then A3:
( dom (FormFunctional (f,g)) = [: the carrier of V, the carrier of W:] & (FormFunctional (f,g)) . (v,w) <> 0. K )
by A1, A2, FUNCT_2:def 1, VECTSP_1:12;
(FormFunctional (f,g)) . ((0. V),(0. W)) =
(f . (0. V)) * (g . (0. W))
by Def10
.=
(0. K) * (g . (0. W))
by HAHNBAN1:def 9
.=
0. K
;
hence
not FormFunctional (f,g) is constant
by A3, BINOP_1:19; verum