let f1, f2 be V8() non trivial linear-Functional of V; :: thesis: ( f1 . v = 1_ K & f1 | the carrier of W = 0Functional W & f2 . v = 1_ K & f2 | the carrier of W = 0Functional W implies f1 = f2 )
assume that
A13:
( f1 . v = 1_ K & f1 | the carrier of W = 0Functional W )
and
A14:
( f2 . v = 1_ K & f2 | the carrier of W = 0Functional W )
; :: thesis: f1 = f2
V is_the_direct_sum_of W, Lin {v}
by VECTSP_5:def 5;
then A15:
( VectSpStr(# the carrier of V,the addF of V,the U2 of V,the lmult of V #) = W + (Lin {v}) & W /\ (Lin {v}) = (0). V )
by VECTSP_5:def 4;
now let w be
Vector of
V;
:: thesis: f1 . w = f2 . w
w in W + (Lin {v})
by A15, STRUCT_0:def 5;
then consider v1,
v2 being
Vector of
V such that A16:
(
v1 in W &
v2 in Lin {v} &
w = v1 + v2 )
by VECTSP_5:5;
consider a being
Element of
K such that A17:
v2 = a * v
by A16, Th4;
A18:
v1 in the
carrier of
W
by A16, STRUCT_0:def 5;
then A19:
f1 . v1 =
(f2 | the carrier of W) . v1
by A13, A14, FUNCT_1:72
.=
f2 . v1
by A18, FUNCT_1:72
;
thus f1 . w =
(f1 . v1) + (f1 . (a * v))
by A16, A17, HAHNBAN1:def 11
.=
(f1 . v1) + (a * (f1 . v))
by HAHNBAN1:def 12
.=
(f1 . v1) + (f2 . (a * v))
by A13, A14, HAHNBAN1:def 12
.=
f2 . w
by A16, A17, A19, HAHNBAN1:def 11
;
:: thesis: verum end;
hence
f1 = f2
by FUNCT_2:113; :: thesis: verum