set fg = FormFunctional f,g;
consider v being Vector of V;
consider w being Vector of W such that
A1: w <> 0. W by STRUCT_0:def 19;
A2: [(0. V),(0. W)] <> [v,w] by A1, ZFMISC_1:33;
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;
assume A4: FormFunctional f,g is trivial ; :: thesis: contradiction

per cases ( FormFunctional f,g = {} or ex x being set st FormFunctional f,g = {x} ) by A4, 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 A2, ZFMISC_1:33; :: thesis: verum

end;

end;