set f = (l * T) +* ((V \ X) --> (0. F));
dom l = [#] W by FUNCT_2:169;
then rng T c= dom l by Th7;
then A2: dom (l * T) = dom T by RELAT_1:46;
A3: dom ((V \ X) --> (0. F)) = ([#] V) \ X by FUNCOP_1:19;
A4: dom T = [#] V by Th7;
([#] V) \/ (([#] V) \ X) = [#] V by XBOOLE_1:12;
then A5: dom ((l * T) +* ((V \ X) --> (0. F))) = [#] V by A2, A3, A4, FUNCT_4:def 1;
A6: rng ((l * T) +* ((V \ X) --> (0. F))) c= (rng (l * T)) \/ (rng ((V \ X) --> (0. F))) by FUNCT_4:18;
A7: rng (l * T) c= rng l by RELAT_1:45;
rng ((V \ X) --> (0. F)) c= {(0. F)} by FUNCOP_1:19;
then A8: rng ((V \ X) --> (0. F)) c= [#] F by XBOOLE_1:1;
rng l c= [#] F by FUNCT_2:169;
then rng (l * T) c= [#] F by A7, XBOOLE_1:1;
then (rng (l * T)) \/ (rng ((V \ X) --> (0. F))) c= [#] F by A8, XBOOLE_1:8;
then rng ((l * T) +* ((V \ X) --> (0. F))) c= [#] F by A6, XBOOLE_1:1;
then reconsider f = (l * T) +* ((V \ X) --> (0. F)) as Element of Funcs ([#] V),([#] F) by A5, FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
f . v = 0. F

proof

set C = { v where v is Element of V : f . v <> 0. F } ;
{ v where v is Element of V : f . v <> 0. F } c= [#] V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of V : f . v <> 0. F } or x in [#] V )
assume A9: x in { v where v is Element of V : f . v <> 0. F } ; :: thesis: x in [#] V
consider v being Element of V such that
A10: v = x and
f . v <> 0. F by A9;
thus x in [#] V by A10; :: thesis: verum

end;

then reconsider C = { v where v is Element of V : f . v <> 0. F } as Subset of V ;
C is finite

proof

card C c= card (Carrier l)

proof

ex g being Function st
( g is one-to-one & dom g = C & rng g c= Carrier l )

proof

set S = (T " (Carrier l)) /\ X;
set g = T | ((T " (Carrier l)) /\ X);
A11: (T " (Carrier l)) /\ X = C

proof

A12: (T " (Carrier l)) /\ X c= C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (T " (Carrier l)) /\ X or x in C )
assume A13: x in (T " (Carrier l)) /\ X ; :: thesis: x in C
A14: x in X by A13, XBOOLE_0:def 4;
A15: x in T " (Carrier l) by A13, XBOOLE_0:def 4;
then A16: x in dom T by FUNCT_1:def 13;
A17: T . x in Carrier l by A15, FUNCT_1:def 13;
reconsider x = x as Element of V by A13;
not x in dom ((V \ X) --> (0. F)) by A14, XBOOLE_0:def 5;
then A18: f . x = (l * T) . x by FUNCT_4:12;
A19: (l * T) . x = l . (T . x) by A16, FUNCT_1:23;
l . (T . x) <> 0. F by A17, VECTSP_6:20;
hence x in C by A18, A19; :: thesis: verum

end;

C c= (T " (Carrier l)) /\ X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in (T " (Carrier l)) /\ X )
assume A20: x in C ; :: thesis: x in (T " (Carrier l)) /\ X
consider v being Element of V such that
A21: v = x and
A22: f . v <> 0. F by A20;
reconsider x = x as Element of V by A21;

A23: now

assume not x in X ; :: thesis: contradiction
then A24: x in V \ X by XBOOLE_0:def 5;
then x in dom ((V \ X) --> (0. F)) by FUNCOP_1:19;
then f . x = ((V \ X) --> (0. F)) . x by FUNCT_4:14;
hence contradiction by A21, A22, A24, FUNCOP_1:13; :: thesis: verum

end;

x in T " (Carrier l)

proof

A25: dom T = [#] V by Th7;
T . x in Carrier l

proof

not x in V \ X by A23, XBOOLE_0:def 5;
then A26: f . x = (l * T) . x by A3, FUNCT_4:12;
(l * T) . x = l . (T . x) by A25, FUNCT_1:23;
hence T . x in Carrier l by A21, A22, A26; :: thesis: verum

end;

hence x in T " (Carrier l) by A25, FUNCT_1:def 13; :: thesis: verum

end;

hence x in (T " (Carrier l)) /\ X by A23, XBOOLE_0:def 4; :: thesis: verum

end;

hence (T " (Carrier l)) /\ X = C by A12, XBOOLE_0:def 10; :: thesis: verum

end;

A27: dom (T | ((T " (Carrier l)) /\ X)) = (T " (Carrier l)) /\ X

proof

dom T = [#] V by Th7;
hence dom (T | ((T " (Carrier l)) /\ X)) = (T " (Carrier l)) /\ X by RELAT_1:91; :: thesis: verum

end;

A28: rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (T | ((T " (Carrier l)) /\ X)) or y in Carrier l )
assume A29: y in rng (T | ((T " (Carrier l)) /\ X)) ; :: thesis: y in Carrier l
consider x being set such that
A30: x in dom (T | ((T " (Carrier l)) /\ X)) and
A31: y = (T | ((T " (Carrier l)) /\ X)) . x by A29, FUNCT_1:def 5;
x in T " (Carrier l) by A27, A30, XBOOLE_0:def 4;
then T . x in Carrier l by FUNCT_1:def 13;
hence y in Carrier l by A27, A30, A31, FUNCT_1:72; :: thesis: verum

end;

take T | ((T " (Carrier l)) /\ X) ; :: thesis: ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l )
thus ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l ) by A1, A11, A27, A28, Th2, XBOOLE_1:17; :: thesis: verum

end;

hence card C c= card (Carrier l) by CARD_1:26; :: thesis: verum

end;

hence C is finite ; :: thesis: verum

end;

then reconsider C = C as finite Subset of V ;
take C ; :: thesis: for v being Element of V st not v in C holds
f . v = 0. F
thus for v being Element of V st not v in C holds
f . v = 0. F ; :: thesis: verum

end;

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 4;
Carrier f c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier f or x in X )
assume A32: x in Carrier f ; :: thesis: x in X
reconsider x = x as Element of V by A32;

now

assume not x in X ; :: thesis: contradiction
then A33: x in V \ X by XBOOLE_0:def 5;
then f . x = ((V \ X) --> (0. F)) . x by A3, FUNCT_4:14
.= 0. F by A33, FUNCOP_1:13 ;
hence contradiction by A32, VECTSP_6:20; :: thesis: verum

end;

hence x in X ; :: thesis: verum

end;

hence (l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X by VECTSP_6:def 7; :: thesis: verum