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