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

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;

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;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