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