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
; contradiction
per cases
( FormFunctional (f,g) = {} or ex x being object st FormFunctional (f,g) = {x} )
by A4, ZFMISC_1:131;
suppose
ex
x being
object st
FormFunctional (
f,
g)
= {x}
;
contradictionthen 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;
verum end; end;