let X be RealNormSpace; :: thesis: for w being Point of X

for e being Real

for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let w be Point of X; :: thesis: for e being Real

for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let e be Real; :: thesis: for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let l be Linear_Combination of {w}; :: thesis: ( 0 < e implies ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )

assume A1: 0 < e ; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

A2: Carrier l c= {w} by RLVECT_2:def 6;

for e being Real

for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let w be Point of X; :: thesis: for e being Real

for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let e be Real; :: thesis: for l being Linear_Combination of {w} st 0 < e holds

ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

let l be Linear_Combination of {w}; :: thesis: ( 0 < e implies ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e ) )

assume A1: 0 < e ; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

A2: Carrier l c= {w} by RLVECT_2:def 6;

per cases
( not w in Carrier l or w in Carrier l )
;

end;

suppose A3:
not w in Carrier l
; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

set m = l;

take l ; :: thesis: ( Carrier l = Carrier l & rng l c= RAT & ||.((Sum l) - (Sum l)).|| < e )

thus Carrier l = Carrier l ; :: thesis: ( rng l c= RAT & ||.((Sum l) - (Sum l)).|| < e )

for y being object st y in rng l holds

y in RAT

(Sum l) - (Sum l) = 0. X by RLVECT_1:15;

hence ||.((Sum l) - (Sum l)).|| < e by A1; :: thesis: verum

end;take l ; :: thesis: ( Carrier l = Carrier l & rng l c= RAT & ||.((Sum l) - (Sum l)).|| < e )

thus Carrier l = Carrier l ; :: thesis: ( rng l c= RAT & ||.((Sum l) - (Sum l)).|| < e )

for y being object st y in rng l holds

y in RAT

proof

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

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

then consider x being object such that

A4: ( x in dom l & y = l . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A4;

not x in Carrier l by A2, A3, TARSKI:def 1;

then y is integer by A4;

hence y in RAT by NUMBERS:14; :: thesis: verum

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

then consider x being object such that

A4: ( x in dom l & y = l . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A4;

not x in Carrier l by A2, A3, TARSKI:def 1;

then y is integer by A4;

hence y in RAT by NUMBERS:14; :: thesis: verum

(Sum l) - (Sum l) = 0. X by RLVECT_1:15;

hence ||.((Sum l) - (Sum l)).|| < e by A1; :: thesis: verum

suppose A5:
w in Carrier l
; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

then A6:
( Carrier l = {w} & l . w <> 0 )
by RLVECT_2:19, RLVECT_2:def 6, ZFMISC_1:31;

end;per cases
( w = 0. X or w <> 0. X )
;

end;

suppose A7:
w = 0. X
; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

A8:
Sum l = (l . w) * w
by RLVECT_2:32;

set m = (1 / (l . w)) * l;

Carrier ((1 / (l . w)) * l) = Carrier l by A6, RLVECT_2:42;

then reconsider m = (1 / (l . w)) * l as Linear_Combination of {w} by RLVECT_2:def 6;

take m ; :: thesis: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

thus Carrier m = Carrier l by A6, 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 = (1 / (l . w)) * (Sum l) by RLVECT_3:2;

hence ||.((Sum l) - (Sum m)).|| < e by A1, A7, A8; :: thesis: verum

end;set m = (1 / (l . w)) * l;

Carrier ((1 / (l . w)) * l) = Carrier l by A6, RLVECT_2:42;

then reconsider m = (1 / (l . w)) * l as Linear_Combination of {w} by RLVECT_2:def 6;

take m ; :: thesis: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

thus Carrier m = Carrier l by A6, 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

A9: ( x in dom m & y = m . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A9;

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

then consider x being object such that

A9: ( x in dom m & y = m . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A9;

per cases
( not x in Carrier l or x in Carrier l )
;

end;

suppose
not x in Carrier l
; :: thesis: y in RAT

then A10:
l . x = 0
;

y = (1 / (l . w)) * (l . x) by A9, RLVECT_2:def 11;

then y is integer by A10;

hence y in RAT by NUMBERS:14; :: thesis: verum

end;y = (1 / (l . w)) * (l . x) by A9, RLVECT_2:def 11;

then y is integer by A10;

hence y in RAT by NUMBERS:14; :: thesis: verum

suppose
x in Carrier l
; :: thesis: y in RAT

then
x = w
by A6, TARSKI:def 1;

then y = (1 / (l . w)) * (l . w) by A9, RLVECT_2:def 11;

then y is integer by A5, RLVECT_2:19, XCMPLX_1:87;

hence y in RAT by NUMBERS:14; :: thesis: verum

end;then y = (1 / (l . w)) * (l . w) by A9, RLVECT_2:def 11;

then y is integer by A5, RLVECT_2:19, XCMPLX_1:87;

hence y in RAT by NUMBERS:14; :: thesis: verum

Sum m = (1 / (l . w)) * (Sum l) by RLVECT_3:2;

hence ||.((Sum l) - (Sum m)).|| < e by A1, A7, A8; :: thesis: verum

suppose A11:
w <> 0. X
; :: thesis: ex m being Linear_Combination of {w} st

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

then A12:
||.w.|| <> 0
by NORMSP_0:def 5;

then consider q being Element of RAT such that

A13: ( q <> 0 & |.((l . w) - q).| < e / ||.w.|| ) by A1, Th21;

set m = (q / (l . w)) * l;

Carrier ((q / (l . w)) * l) = Carrier l by A6, A13, RLVECT_2:42;

then reconsider m = (q / (l . w)) * l as Linear_Combination of {w} by RLVECT_2:def 6;

take m ; :: thesis: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

thus Carrier m = Carrier l by A6, A13, 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

A16: Sum m = (q / (l . w)) * (Sum l) by RLVECT_3:2

.= (q / (l . w)) * ((l . w) * w) by RLVECT_2:32

.= ((q / (l . w)) * (l . w)) * w by RLVECT_1:def 7

.= q * w by A5, RLVECT_2:19, XCMPLX_1:87 ;

(Sum l) - (Sum m) = ((l . w) * w) - (Sum m) by RLVECT_2:32

.= ((l . w) - q) * w by A16, RLVECT_1:35 ;

then A17: ||.((Sum l) - (Sum m)).|| = |.((l . w) - q).| * ||.w.|| by NORMSP_1:def 1;

|.((l . w) - q).| * ||.w.|| < (e / ||.w.||) * ||.w.|| by A12, A13, XREAL_1:68;

hence ||.((Sum l) - (Sum m)).|| < e by A11, A17, NORMSP_0:def 5, XCMPLX_1:87; :: thesis: verum

end;then consider q being Element of RAT such that

A13: ( q <> 0 & |.((l . w) - q).| < e / ||.w.|| ) by A1, Th21;

set m = (q / (l . w)) * l;

Carrier ((q / (l . w)) * l) = Carrier l by A6, A13, RLVECT_2:42;

then reconsider m = (q / (l . w)) * l as Linear_Combination of {w} by RLVECT_2:def 6;

take m ; :: thesis: ( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )

thus Carrier m = Carrier l by A6, A13, 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

A14: ( x in dom m & y = m . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A14;

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

then consider x being object such that

A14: ( x in dom m & y = m . x ) by FUNCT_1:def 3;

reconsider x = x as Point of X by A14;

per cases
( not x in Carrier l or x in Carrier l )
;

end;

suppose
not x in Carrier l
; :: thesis: y in RAT

then A15:
l . x = 0
;

y = (q / (l . w)) * (l . x) by A14, RLVECT_2:def 11;

then y is integer by A15;

hence y in RAT by NUMBERS:14; :: thesis: verum

end;y = (q / (l . w)) * (l . x) by A14, RLVECT_2:def 11;

then y is integer by A15;

hence y in RAT by NUMBERS:14; :: thesis: verum

suppose
x in Carrier l
; :: thesis: y in RAT

then
x = w
by A6, TARSKI:def 1;

then y = (q / (l . w)) * (l . w) by A14, RLVECT_2:def 11;

then y = q by A5, RLVECT_2:19, XCMPLX_1:87;

hence y in RAT ; :: thesis: verum

end;then y = (q / (l . w)) * (l . w) by A14, RLVECT_2:def 11;

then y = q by A5, RLVECT_2:19, XCMPLX_1:87;

hence y in RAT ; :: thesis: verum

A16: Sum m = (q / (l . w)) * (Sum l) by RLVECT_3:2

.= (q / (l . w)) * ((l . w) * w) by RLVECT_2:32

.= ((q / (l . w)) * (l . w)) * w by RLVECT_1:def 7

.= q * w by A5, RLVECT_2:19, XCMPLX_1:87 ;

(Sum l) - (Sum m) = ((l . w) * w) - (Sum m) by RLVECT_2:32

.= ((l . w) - q) * w by A16, RLVECT_1:35 ;

then A17: ||.((Sum l) - (Sum m)).|| = |.((l . w) - q).| * ||.w.|| by NORMSP_1:def 1;

|.((l . w) - q).| * ||.w.|| < (e / ||.w.||) * ||.w.|| by A12, A13, XREAL_1:68;

hence ||.((Sum l) - (Sum m)).|| < e by A11, A17, NORMSP_0:def 5, XCMPLX_1:87; :: thesis: verum