set fg = FrFormFunctional (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 (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) & [[v, the Vector of W],((FrFormFunctional (f,g)) . (v, the Vector of 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 = [[v, the Vector of W],((FrFormFunctional (f,g)) . (v, the Vector of W))] ) by A3, A5, TARSKI:def 1;
hence contradiction by A2, XTUPLE_0:1; :: thesis: verum

end;

end;