set fg = FormFunctional (f,g);
consider v being Vector of V such that
v <> 0. V
and
A1:
f . v <> 0. K
by VECTSP10:29;
consider w being Vector of W such that
w <> 0. W
and
A2:
g . w <> 0. K
by VECTSP10:29;
(FormFunctional (f,g)) . (v,w) = (f . v) * (g . w)
by Def11;
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:44;
(FormFunctional (f,g)) . ((0. V),(0. W)) =
(f . (0. V)) * (g . (0. W))
by Def11
.=
(0. K) * (g . (0. W))
by HAHNBAN1:def 13
.=
0. K
by VECTSP_1:39
;
hence
not FormFunctional (f,g) is constant
by A3, BINOP_1:31; verum