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 ;
then dom ((l * T) +* ((X `) --> (0. R))) = [#] V by ;
then reconsider f = (l * T) +* ((X `) --> (0. R)) as Element of Funcs (([#] V), the carrier of R) by ;
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 " ()) /\ X;
set g = T | ((T " ()) /\ X);
take T | ((T " ()) /\ X) ; :: thesis: ( T | ((T " ()) /\ X) is one-to-one & dom (T | ((T " ()) /\ X)) = C & rng (T | ((T " ()) /\ X)) c= Carrier l )
A6: C c= (T " ()) /\ X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in (T " ()) /\ X )
assume A7: x in C ; :: thesis: x in (T " ()) /\ 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;
then not x in X ` by XBOOLE_0:def 5;
then A11: f . x = (l * T) . x by ;
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 ;
then x in T " () by ;
hence x in (T " ()) /\ X by ; :: thesis: verum
end;
A13: dom T = [#] V by RANKNULL:7;
A14: rng (T | ((T " ()) /\ X)) c= Carrier l
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (T | ((T " ()) /\ X)) or y in Carrier l )
assume y in rng (T | ((T " ()) /\ X)) ; :: thesis:
then consider x being object such that
A15: x in dom (T | ((T " ()) /\ X)) and
A16: y = (T | ((T " ()) /\ X)) . x by FUNCT_1:def 3;
x in T " () by ;
then T . x in Carrier l by FUNCT_1:def 7;
hence y in Carrier l by ; :: thesis: verum
end;
(T " ()) /\ X c= C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (T " ()) /\ X or x in C )
assume A17: x in (T " ()) /\ X ; :: thesis: x in C
A18: x in X by ;
A19: x in T " () by ;
then A20: x in dom T by FUNCT_1:def 7;
A21: T . x in Carrier l by ;
reconsider x = x as Element of V by A17;
A22: l . (T . x) <> 0. R by ;
not x in dom ((X `) --> (0. R)) by ;
then A23: f . x = (l * T) . x by FUNCT_4:11;
(l * T) . x = l . (T . x) by ;
hence x in C by ; :: thesis: verum
end;
hence ( T | ((T " ()) /\ X) is one-to-one & dom (T | ((T " ()) /\ X)) = C & rng (T | ((T " ()) /\ X)) c= Carrier l ) by ; :: thesis: verum
end;
then card C c= card () 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
.= 0. R by ;
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