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; :: thesis: verum

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; :: thesis: verum