let X be RealNormSpace; :: thesis: for A being Subset of X
for e being Real
for l being Linear_Combination of A st 0 < e holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let A be Subset of X; :: thesis: for e being Real
for l being Linear_Combination of A st 0 < e holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

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

let l be Linear_Combination of A; :: thesis: ( 0 < e & card () = 0 implies ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )

assume A2: ( 0 < e & card () = 0 ) ; :: thesis: ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

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: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
thus Carrier m = Carrier l by RLVECT_2:42; :: thesis: ( rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )
for y being object st y in rng m holds
y in RAT
proof
let y be object ; :: thesis: ( y in rng m implies y in RAT )
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 ;
then y is integer by A5;
hence y in RAT by NUMBERS:14; :: thesis: verum
end;
hence rng m c= RAT ; :: thesis: ||.((Sum l) - (Sum m)).|| < e
Sum m = a * (Sum l) by RLVECT_3:2;
hence ||.((Sum l) - (Sum m)).|| < e by A2, A3; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
let e be Real; :: thesis: for l being Linear_Combination of A st 0 < e & card () = k + 1 holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let l be Linear_Combination of A; :: thesis: ( 0 < e & card () = k + 1 implies ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )

assume A8: ( 0 < e & card () = k + 1 ) ; :: thesis: ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

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 (() \ {w}) = (card ()) - () by
.= (k + 1) - 1 by ;
reconsider A0 = () \ {w} as finite Subset of X ;
reconsider B0 = {w} as finite Subset of X ;
A0 \/ B0 = () \/ B0 by XBOOLE_1:39;
then A0 \/ B0 = Carrier l by ;
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 = () \ B0 & Carrier l2 = () \ A0 ) by ;
A14: Carrier l c= A by RLVECT_2:def 6;
Carrier l1 c= Carrier l by ;
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 ;
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 ;
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 ;
A19: m is Linear_Combination of A by ;
(Sum l) - (Sum m) = ((Sum l1) + (Sum l2)) - (Sum m) by
.= (((Sum l1) + (Sum l2)) - (Sum m1)) - (Sum m2) by
.= ((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 ;
then ||.((Sum l) - (Sum m)).|| < e by ;
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: verum
end;
A21: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A6);
let e be Real; :: thesis: for l being Linear_Combination of A st 0 < e holds
ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let l be Linear_Combination of A; :: thesis: ( 0 < e implies ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )

assume A22: 0 < e ; :: thesis: ex m being Linear_Combination of A st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

card () 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 ; :: thesis: verum