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 S_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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 (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: verum

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 S

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

proof

A6:
for k being Nat st S
let e be Real; :: thesis: for l being Linear_Combination of A st 0 < e & card (Carrier l) = 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 (Carrier l) = 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 (Carrier l) = 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

Sum m = a * (Sum l) by RLVECT_3:2;

hence ||.((Sum l) - (Sum m)).|| < e by A2, A3; :: thesis: verum

end;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 (Carrier l) = 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 (Carrier l) = 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

hence
rng m c= RAT
; :: thesis: ||.((Sum l) - (Sum m)).|| < e
let y be object ; :: thesis: ( y in rng m implies y in RAT )

assume y in rng m ; :: thesis: y in RAT

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: verum

end;assume y in rng m ; :: thesis: y in RAT

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: verum

Sum m = a * (Sum l) by RLVECT_3:2;

hence ||.((Sum l) - (Sum m)).|| < e by A2, A3; :: thesis: verum

S

proof

A21:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let e be Real; :: thesis: for l being Linear_Combination of A st 0 < e & card (Carrier l) = 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 (Carrier l) = 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 (Carrier l) = 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 ((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: verum

end;assume A7: S

let e be Real; :: thesis: for l being Linear_Combination of A st 0 < e & card (Carrier l) = 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 (Carrier l) = 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 (Carrier l) = 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 ((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: verum

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 (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: verum