consider v being Vector of V such that
A1: ( v <> 0. V & f . v <> 0. K ) by VECTSP10:29;
consider w being Vector of W such that
A2: ( w <> 0. W & g . w <> 0. K ) by VECTSP10:29;
set fg = FormFunctional f,g;
A3: (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 ;
A4: dom (FormFunctional f,g) = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
(FormFunctional f,g) . v,w = (f . v) * (g . w) by Def11;
then (FormFunctional f,g) . v,w <> 0. K by A1, A2, VECTSP_1:44;
hence not FormFunctional f,g is constant by A3, A4, BINOP_1:31; :: thesis: verum