let X be RealNormSpace; :: thesis:
let A be Subset of X; :: thesis:
defpred S₁[ Nat] means for e being Real
for l being Linear_Combination of A st 0 < e & card (Carrier l) = $1 holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e );
A1: S₁[ 0 ]

let e be Real; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A2: ( 0 < e & card (Carrier l) = 0 ) ; :: thesis:
then Carrier l = {} ;
then A3: Sum l = 0. X by RLVECT_2:34;
reconsider a = 1 as Real ;
reconsider m = a * l as Linear_Combination of A by RLVECT_2:44;
take m ; :: thesis:
thus Carrier m = Carrier l by RLVECT_2:42; :: thesis:
for y being object st y in rng m holds
y in RAT

let y be object ; :: thesis:
assume y in rng m ; :: thesis:
then consider x being object such that
A4: ( x in dom m & y = m . x ) by FUNCT_1:def 3;
reconsider x = x as Point of X by A4;
A5: not x in Carrier l by A2;
y = a * (l . x) by A4, RLVECT_2:def 11;
then y is integer by A5;
hence y in RAT by NUMBERS:14; :: thesis:

end;

hence rng m c= RAT ; :: thesis:
Sum m = a * (Sum l) by RLVECT_3:2;
hence ||.((Sum l) - (Sum m)).|| < e by A2, A3; :: thesis:

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A7: S₁[k] ; :: thesis:
let e be Real; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A8: ( 0 < e & card (Carrier l) = k + 1 ) ; :: thesis:
then Carrier l <> {} ;
then consider w being object such that
A9: w in Carrier l by XBOOLE_0:def 1;
reconsider w = w as Element of the carrier of X by A9;
A10: card ((Carrier l) \ {w}) = (card (Carrier l)) - (card {w}) by A9, CARD_2:44, ZFMISC_1:31
.= (k + 1) - 1 by A8, CARD_2:42 ;
reconsider A0 = (Carrier l) \ {w} as finite Subset of X ;
reconsider B0 = {w} as finite Subset of X ;
A0 \/ B0 = (Carrier l) \/ B0 by XBOOLE_1:39;
then A0 \/ B0 = Carrier l by A9, XBOOLE_1:12, ZFMISC_1:31;
then A11: l is Linear_Combination of A0 \/ B0 by RLVECT_2:def 6;
consider l1 being Linear_Combination of A0, l2 being Linear_Combination of B0 such that
A13: ( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B0 & Carrier l2 = (Carrier l) \ A0 ) by A11, Th9, XBOOLE_1:79;
A14: Carrier l c= A by RLVECT_2:def 6;
Carrier l1 c= Carrier l by A13, XBOOLE_1:36;
then Carrier l1 c= A by A14;
then l1 is Linear_Combination of A by RLVECT_2:def 6;
then consider m1 being Linear_Combination of A such that
A15: ( Carrier m1 = Carrier l1 & rng m1 c= RAT & ||.((Sum l1) - (Sum m1)).|| < e / 2 ) by A7, A8, A10, A13;
A16: m1 is Linear_Combination of A0 by A15, RLVECT_2:def 6;
consider m2 being Linear_Combination of {w} such that
A17: ( Carrier m2 = Carrier l2 & rng m2 c= RAT & ||.((Sum l2) - (Sum m2)).|| < e / 2 ) by A8, Th22;
consider m being Linear_Combination of A0 \/ {w} such that
A18: ( Carrier m = (Carrier m1) \/ (Carrier m2) & rng m c= RAT & Sum m = (Sum m1) + (Sum m2) ) by XBOOLE_1:79, A15, A16, A17, Th10;
A19: m is Linear_Combination of A by A13, A15, A17, A18, RLVECT_2:def 6;
(Sum l) - (Sum m) = ((Sum l1) + (Sum l2)) - (Sum m) by A13, RLVECT_3:1
.= (((Sum l1) + (Sum l2)) - (Sum m1)) - (Sum m2) by A18, RLVECT_1:27
.= ((Sum l2) + ((Sum l1) - (Sum m1))) - (Sum m2) by RLVECT_1:28
.= ((Sum l1) - (Sum m1)) + ((Sum l2) - (Sum m2)) by RLVECT_1:28 ;
then A20: ||.((Sum l) - (Sum m)).|| <= ||.((Sum l1) - (Sum m1)).|| + ||.((Sum l2) - (Sum m2)).|| by NORMSP_1:def 1;
||.((Sum l1) - (Sum m1)).|| + ||.((Sum l2) - (Sum m2)).|| < (e / 2) + (e / 2) by A15, A17, XREAL_1:8;
then ||.((Sum l) - (Sum m)).|| < e by A20, XXREAL_0:2;
hence ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) by A13, A15, A17, A18, A19; :: thesis:

end;

A21: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A6);
let e be Real; :: thesis:
let l be Linear_Combination of A; :: thesis:
assume A22: 0 < e ; :: thesis:
card (Carrier l) is Nat ;
hence ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) by A21, A22; :: thesis: