set fg = FrFormFunctional (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 (FrFormFunctional (f,g)) = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
then A3: ( [[(0. V),(0. W)],((FrFormFunctional (f,g)) . ((0. V),(0. W)))] in FrFormFunctional (f,g) & [[ the Vector of V,w],((FrFormFunctional (f,g)) . ( the Vector of V,w))] in FrFormFunctional (f,g) ) by FUNCT_1:1;
assume A4: FrFormFunctional (f,g) is trivial ; :: thesis: contradiction

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

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

hence contradiction ; :: thesis: verum

end;

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

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

end;

end;