consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def 19;
consider w being Vector of W;
set fg = FormFunctional f,g;
assume A2: FormFunctional f,g is trivial ; :: thesis: contradiction
dom (FormFunctional f,g) = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
then A3: ( [[(0. V),(0. W)],((FormFunctional f,g) . (0. V),(0. W))] in FormFunctional f,g & [[v,w],((FormFunctional f,g) . v,w)] in FormFunctional f,g ) by FUNCT_1:8;
A4: [(0. V),(0. W)] <> [v,w] by A1, ZFMISC_1:33;

per cases ( FormFunctional f,g = {} or ex x being set st FormFunctional f,g = {x} ) by A2, REALSET1:def 4;

suppose FormFunctional f,g = {} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose ex x being set st FormFunctional f,g = {x} ; :: thesis: contradiction

then consider x being set such that
A5: FormFunctional f,g = {x} ;
( [[(0. V),(0. W)],((FormFunctional f,g) . (0. V),(0. W))] = x & x = [[v,w],((FormFunctional f,g) . v,w)] ) by A3, A5, TARSKI:def 1;
hence contradiction by A4, ZFMISC_1:33; :: thesis: verum

end;

end;