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 )

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((Rseq . (n1,n2)) - r).| < 1 / m ) by Th57; :: thesis: verum

( 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

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 }

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 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 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 ) 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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum

end;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

hence
for m being non zero Nat ex n 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

|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum

end;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

hence
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
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;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

|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((Rseq . (n1,n2)) - r).| < 1 / m ; :: thesis: verum

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 }

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 }

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;

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;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 }

hence
ex n 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 }

end;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;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

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

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

for n1, n2 being Nat st n <= n1 & n <= n2 holds

|.((Rseq . (n1,n2)) - r).| < 1 / m ) by Th57; :: thesis: verum