reconsider SZ0 = {(0. R)} as finite Subset of R ;
dom l = [#] W by FUNCT_2:92;
then rng T c= dom l ;
then A3: dom (l * T) = dom T by RELAT_1:27;
set f = (l * T) +* ((X `) --> (0. R));
A4: dom ((X `) --> (0. R)) = X ` ;
( rng ((l * T) +* ((X `) --> (0. R))) c= (rng (l * T)) \/ (rng ((X `) --> (0. R))) & (rng (l * T)) \/ (rng ((X `) --> (0. R))) c= the carrier of R ) by FUNCT_4:17;
then A5: rng ((l * T) +* ((X `) --> (0. R))) c= the carrier of R ;
( dom T = [#] V & ([#] V) \/ (([#] V) \ X) = [#] V ) by RANKNULL:7, XBOOLE_1:12;
then dom ((l * T) +* ((X `) --> (0. R))) = [#] V by A3, A4, FUNCT_4:def 1;
then reconsider f = (l * T) +* ((X `) --> (0. R)) as Element of Funcs (([#] V), the carrier of R) 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. R

proof

set C = { v where v is Element of V : f . v <> 0. R } ;
{ v where v is Element of V : f . v <> 0. R } 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. R } or x in [#] V )
assume x in { v where v is Element of V : f . v <> 0. R } ; :: thesis: x in [#] V
then ex v being Element of V st
( v = x & f . v <> 0. R ) ;
hence x in [#] V ; :: thesis: verum

end;

then reconsider C = { v where v is Element of V : f . v <> 0. R } 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. R ) 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 X ` by XBOOLE_0:def 5;
then x in dom ((X `) --> (0. R)) ;
then f . x = ((X `) --> (0. R)) . x by FUNCT_4:13;
hence contradiction by A8, A10, FUNCOP_1:7; :: thesis: verum

end;

then not x in X ` by XBOOLE_0:def 5;
then A11: f . x = (l * T) . x by A4, FUNCT_4:11;
A12: dom T = [#] V by RANKNULL:7;
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 RANKNULL:7;
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. R by A21, ZMODUL02:8;
not x in dom ((X `) --> (0. R)) 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 A22, A23; :: thesis: verum

end;

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, A6, A13, A14, RANKNULL:2, 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. R
thus for v being Element of V st not v in C holds
f . v = 0. R ; :: 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 X ` by XBOOLE_0:def 5;
then f . x = ((X `) --> (0. R)) . x by A4, FUNCT_4:13
.= 0. R by A25, FUNCOP_1:7 ;
hence contradiction by A24, ZMODUL02:8; :: thesis: verum

end;

hence x in X ; :: thesis: verum

end;

hence (l * T) +* ((X `) --> (0. R)) is Linear_Combination of X by VECTSP_6:def 4; :: thesis: verum