let r be Real; :: thesis: for Rseq being Function of [:NAT,NAT:],REAL holds
( r in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m )
let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( r in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m )
reconsider p = r as Point of RealSpace by XREAL_0:def 1;
( ( for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } ) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m )
proof
hereby :: thesis: ( ( for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m ) implies for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } )
assume A1: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } ; :: thesis: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m
now :: thesis: for m being non zero Nat ex n0 being Nat st
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m
let m be non zero Nat; :: thesis: ex n0 being Nat st
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m
consider n0 being Nat such that
A2: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } by A1;
take n0 = n0; :: thesis: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m
proof
let n1, n2 be Nat; :: thesis: ( n0 <= n1 & n0 <= n2 implies |.((Rseq . (n1,n2)) - r).| < 1 / m )
assume ( n0 <= n1 & n0 <= n2 ) ; :: thesis: |.((Rseq . (n1,n2)) - r).| < 1 / m
then Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } by A2;
then consider q being Point of RealSpace such that
A3: Rseq . (n1,n2) = q and
A4: dist (p,q) < 1 / m ;
reconsider qr = q as Real ;
ex xr, yr being Real st
( p = xr & q = yr & dist (p,q) = real_dist . (p,q) & dist (p,q) = (Pitag_dist 1) . (<*p*>,<*q*>) & dist (p,q) = |.(xr - yr).| ) by Th6;
hence |.((Rseq . (n1,n2)) - r).| < 1 / m by A3, A4, COMPLEX1:60; :: thesis: verum
end;
hence for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum
end;
hence for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum
end;
assume A5: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
now :: thesis: for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
let m be non zero Nat; :: thesis: ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
consider n0 being Nat such that
A6: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m by A5;
now :: thesis: ex n0 being Nat st
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
take n0 = n0; :: thesis: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
hereby :: thesis: verum
let n1, n2 be Nat; :: thesis: ( n0 <= n1 & n0 <= n2 implies Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } )
assume ( n0 <= n1 & n0 <= n2 ) ; :: thesis: Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m }
then A7: |.((Rseq . (n1,n2)) - r).| < 1 / m by A6;
reconsider m1 = n1, m2 = n2 as Element of NAT by ORDINAL1:def 12;
Rseq . (m1,m2) in the carrier of RealSpace ;
then reconsider q = Rseq . (n1,n2) as Point of RealSpace ;
consider xr, yr being Real such that
A8: p = xr and
A9: q = yr and
dist (p,q) = real_dist . (p,q) and
dist (p,q) = (Pitag_dist 1) . (<*p*>,<*q*>) and
A10: dist (p,q) = |.(xr - yr).| by Th6;
|.(xr - yr).| < 1 / m by A8, A9, A7, COMPLEX1:60;
hence Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } by A10; :: thesis: verum
end;
end;
hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } ; :: thesis: verum
end;
hence for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
Rseq . (n1,n2) in { q where q is Point of RealSpace : dist (p,q) < 1 / m } ; :: thesis: verum
end;
hence ( r in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
|.((Rseq . (n1,n2)) - r).| < 1 / m ) by Th57; :: thesis: verum