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

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { v where v is Element of V : f . v <> 0. R } ; :: thesis:
then ex v being Element of V st
( v = x & f . v <> 0. R ) ;
hence x in [#] V ; :: thesis:

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 )

set S = (T " (Carrier l)) /\ X;
set g = T | ((T " (Carrier l)) /\ X);
take T | ((T " (Carrier l)) /\ X) ; :: thesis:
A6: C c= (T " (Carrier l)) /\ X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A7: x in C ; :: thesis:
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;

end;

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (T | ((T " (Carrier l)) /\ X)) ; :: thesis:
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:

end;

end;

end;

then card C c= card (Carrier l) by CARD_1:10;
then reconsider C = C as finite Subset of V ;
take C ; :: thesis:
thus for v being Element of V st not v in C holds
f . v = 0. R ; :: thesis:

end;

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

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

end;

end;