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