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;

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

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 )

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

proof

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;

hence rng l c= RAT ; :: thesis: ||.((Sum l) - (Sum l)).|| < e
(Sum l) - (Sum l) = 0. X by RLVECT_1:15;
hence ||.((Sum l) - (Sum l)).|| < e by A1; :: thesis: verum

end;

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 )

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

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

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 )

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

proof

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;

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

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;

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;

end;

end;

hence rng m c= RAT ; :: thesis: ||.((Sum l) - (Sum m)).|| < e
Sum m = (1 / (l . w)) * (Sum l) by RLVECT_3:2;
hence ||.((Sum l) - (Sum m)).|| < e by A1, A7, A8; :: thesis: verum

end;

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 )

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

proof

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;

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

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;

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;

end;

end;

hence rng m c= RAT ; :: thesis: ||.((Sum l) - (Sum m)).|| < e
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;

end;

end;

end;