set fg = FormFunctional (f,g);

set w = the Vector of W;

consider v being Vector of V such that

A1: v <> 0. V by STRUCT_0:def 18;

A2: [(0. V),(0. W)] <> [v, the Vector of 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) & [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of W))] in FormFunctional (f,g) ) by FUNCT_1:1;

assume A4: FormFunctional (f,g) is trivial ; :: thesis: contradiction

set w = the Vector of W;

consider v being Vector of V such that

A1: v <> 0. V by STRUCT_0:def 18;

A2: [(0. V),(0. W)] <> [v, the Vector of 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) & [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of 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;

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 = [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of W))] ) by A3, A5, TARSKI:def 1;

hence contradiction by A2, XTUPLE_0:1; :: thesis: verum

end;A5: FormFunctional (f,g) = {x} ;

( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] = x & x = [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of W))] ) by A3, A5, TARSKI:def 1;

hence contradiction by A2, XTUPLE_0:1; :: thesis: verum