( rng (l * T) c= rng l & rng l c= [#] F ) by FUNCT_2:92, RELAT_1:26;
then A2: rng (l * T) c= [#] F ;
dom l = [#] W by FUNCT_2:92;
then rng T c= dom l by Th7;
then A3: dom (l * T) = dom T by RELAT_1:27;
set f = (l * T) +* ((V \ X) --> (0. F));
A4: dom ((V \ X) --> (0. F)) = ([#] V) \ X ;
rng ((V \ X) --> (0. F)) c= {(0. F)} by FUNCOP_1:13;
then rng ((V \ X) --> (0. F)) c= [#] F by XBOOLE_1:1;
then ( rng ((l * T) +* ((V \ X) --> (0. F))) c= (rng (l * T)) \/ (rng ((V \ X) --> (0. F))) & (rng (l * T)) \/ (rng ((V \ X) --> (0. F))) c= [#] F ) by A2, FUNCT_4:17, XBOOLE_1:8;
then A5: rng ((l * T) +* ((V \ X) --> (0. F))) c= [#] F ;
( dom T = [#] V & ([#] V) \/ (([#] V) \ X) = [#] V ) by Th7, XBOOLE_1:12;
then dom ((l * T) +* ((V \ X) --> (0. F))) = [#] V by A3, A4, FUNCT_4:def 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 object ; :: 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 x in { v where v is Element of V : f . v <> 0. F } ; :: thesis: x in [#] V
then ex v being Element of V st
( v = x & f . v <> 0. F ) ;
hence x in [#] V ; :: thesis: verum

end;

then reconsider C = { v where v is Element of V : f . v <> 0. F } as Subset of V ;
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);
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 )
A6: C c= (T " (Carrier l)) /\ X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in (T " (Carrier l)) /\ X )
assume A7: x in C ; :: thesis: x in (T " (Carrier l)) /\ X
A8: ex v being Element of V st
( v = x & f . v <> 0. F ) by A7;
reconsider x = x as Element of V by A7;

A9: now :: thesis: x in X

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

end;

then not x in V \ X by XBOOLE_0:def 5;
then A11: f . x = (l * T) . x by A4, FUNCT_4:11;
A12: dom T = [#] V by Th7;
then (l * T) . x = l . (T . x) by FUNCT_1:13;
then T . x in Carrier l by A8, A11;
then x in T " (Carrier l) by A12, FUNCT_1:def 7;
hence x in (T " (Carrier l)) /\ X by A9, XBOOLE_0:def 4; :: thesis: verum

end;

A13: dom T = [#] V by Th7;
A14: rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (T | ((T " (Carrier l)) /\ X)) or y in Carrier l )
assume y in rng (T | ((T " (Carrier l)) /\ X)) ; :: thesis: y in Carrier l
then consider x being object such that
A15: x in dom (T | ((T " (Carrier l)) /\ X)) and
A16: y = (T | ((T " (Carrier l)) /\ X)) . x by FUNCT_1:def 3;
x in T " (Carrier l) by A15, XBOOLE_0:def 4;
then T . x in Carrier l by FUNCT_1:def 7;
hence y in Carrier l by A15, A16, FUNCT_1:49; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (T " (Carrier l)) /\ X or x in C )
assume A17: x in (T " (Carrier l)) /\ X ; :: thesis: x in C
A18: x in X by A17, XBOOLE_0:def 4;
A19: x in T " (Carrier l) by A17, XBOOLE_0:def 4;
then A20: x in dom T by FUNCT_1:def 7;
A21: T . x in Carrier l by A19, FUNCT_1:def 7;
reconsider x = x as Element of V by A17;
A22: l . (T . x) <> 0. F by A21, VECTSP_6:2;
not x in dom ((V \ X) --> (0. F)) by A18, XBOOLE_0:def 5;
then A23: f . x = (l * T) . x by FUNCT_4:11;
(l * T) . x = l . (T . x) by A20, FUNCT_1:13;
hence x in C by A23, A22; :: thesis: verum

end;

then (T " (Carrier l)) /\ X = C by A6;
hence ( 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, A13, A14, Th2, RELAT_1:62, XBOOLE_1:17; :: thesis: verum

end;

then card C c= card (Carrier l) by CARD_1:10;
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 1;
Carrier f c= X

proof

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

now :: thesis: x in X

assume not x in X ; :: thesis: contradiction
then A25: x in V \ X by XBOOLE_0:def 5;
then f . x = ((V \ X) --> (0. F)) . x by A4, FUNCT_4:13
.= 0. F by A25, FUNCOP_1:7 ;
hence contradiction by A24, VECTSP_6:2; :: 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 4; :: thesis: verum