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

Carrier f c= X

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

then reconsider f = f as Linear_Combination of V by VECTSP_6:def 1;
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

ex g being Function st

( g is one-to-one & dom g = C & rng g c= Carrier l )

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;{ v where v is Element of V : f . v <> 0. R } c= [#] V

proof

then reconsider C = { v where v is Element of V : f . v <> 0. R } as Subset of V ;
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;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

ex g being Function st

( g is one-to-one & dom g = C & rng g c= Carrier l )

proof

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

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

end;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

A13:
dom T = [#] V
by RANKNULL:7;
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;

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;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

then
not x in X `
by XBOOLE_0:def 5;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 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

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

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

proof

(T " (Carrier l)) /\ X c= C
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;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

proof

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
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;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

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

Carrier f c= X

proof

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

end;assume A24: x in Carrier f ; :: thesis: x in X

reconsider x = x as Element of V by A24;

now :: thesis: x in X

hence
x in X
; :: thesis: verumassume
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;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