let f1, f2 be V8() non trivial linear-Functional of V; ( 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
A10:
f1 . v = 1_ K
and
A11:
f1 | the carrier of W = 0Functional W
and
A12:
f2 . v = 1_ K
and
A13:
f2 | the carrier of W = 0Functional W
; f1 = f2
V is_the_direct_sum_of W, Lin {v}
by VECTSP_5:def 5;
then A14:
ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = W + (Lin {v})
;
now for w being Vector of V holds f1 . w = f2 . wlet w be
Vector of
V;
f1 . w = f2 . w
w in W + (Lin {v})
by A14;
then consider v1,
v2 being
Vector of
V such that A15:
v1 in W
and A16:
v2 in Lin {v}
and A17:
w = v1 + v2
by VECTSP_5:1;
consider a being
Element of
K such that A18:
v2 = a * v
by A16, Th3;
A19:
v1 in the
carrier of
W
by A15;
then A20:
f1 . v1 =
(f2 | the carrier of W) . v1
by A11, A13, FUNCT_1:49
.=
f2 . v1
by A19, FUNCT_1:49
;
thus f1 . w =
(f1 . v1) + (f1 . (a * v))
by A17, A18, VECTSP_1:def 20
.=
(f1 . v1) + (a * (f1 . v))
by HAHNBAN1:def 8
.=
(f1 . v1) + (f2 . (a * v))
by A10, A12, HAHNBAN1:def 8
.=
f2 . w
by A17, A18, A20, VECTSP_1:def 20
;
verum end;
hence
f1 = f2
by FUNCT_2:63; verum