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

per cases ( FormFunctional (f,g) = {} or ex x being object st FormFunctional (f,g) = {x} ) by A4, ZFMISC_1:131;

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

hence contradiction ; :: thesis: verum

end;

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

then consider x being object such that
A5: FormFunctional (f,g) = {x} ;
( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] = x & x = [[ the Vector of V,w],((FormFunctional (f,g)) . ( the Vector of V,w))] ) by A3, A5, TARSKI:def 1;
hence contradiction by A2, XTUPLE_0:1; :: thesis: verum

end;

end;