let f be Function of ([#] OrderedNAT),R^1; for seq being Function of NAT,REAL st f = seq & lim_f f <> {} holds
( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) )
let seq be Function of NAT,REAL; ( f = seq & lim_f f <> {} implies ( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) ) )
assume that
A1:
f = seq
and
A2:
lim_f f <> {}
; ( seq is convergent & ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) ) )
consider x being object such that
A3:
x in lim_f f
by A2, XBOOLE_0:def 1;
reconsider y = x as Point of (TopSpaceMetr RealSpace) by A3;
reconsider z = y as Real ;
A4:
Balls y is basis of (BOOL2F (NeighborhoodSystem y))
by CARDFIL3:6;
consider yr being Point of RealSpace such that
A5:
yr = y
and
A6:
Balls y = { (Ball (yr,(1 / n))) where n is Nat : n <> 0 }
by FRECHET:def 1;
A7:
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p
proof
now for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < plet p be
Real;
( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p )assume
0 < p
;
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < pthen consider M being
Nat such that A8:
not
M is
zero
and A9:
1
/ M < p
by Th5;
now ex i0 being Nat st
for m being Nat st i0 <= m holds
|.((seq . m) - z).| < p
Ball (
yr,
(1 / M))
in Balls y
by A8, A6;
then consider i being
Element of
OrderedNAT such that A10:
for
j being
Element of
OrderedNAT st
i <= j holds
f . j in Ball (
yr,
(1 / M))
by A4, A3, CARDFIL2:84;
reconsider i0 =
i as
Nat ;
take i0 =
i0;
for m being Nat st i0 <= m holds
|.((seq . m) - z).| < plet m be
Nat;
( i0 <= m implies |.((seq . m) - z).| < p )assume A11:
i0 <= m
;
|.((seq . m) - z).| < preconsider m0 =
m as
Element of
OrderedNAT by ORDINAL1:def 12;
m0 in { x where x is Element of NAT : ex p0 being Element of NAT st
( i0 = p0 & p0 <= x ) }
by A11;
then
m0 in uparrow i
by CARDFIL2:50;
then
f . m0 in Ball (
yr,
(1 / M))
by A10, WAYBEL_0:18;
then
f . m0 in ].(yr - (1 / M)),(yr + (1 / M)).[
by FRECHET:7;
then A12:
(
yr - (1 / M) < seq . m0 &
seq . m0 < yr + (1 / M) )
by A1, XXREAL_1:4;
(
yr - p < yr - (1 / M) &
yr + (1 / M) < yr + p )
by A9, XREAL_1:8, XREAL_1:15;
then
(
yr - p < seq . m0 &
seq . m0 < yr + p )
by A12, XXREAL_0:2;
then
seq . m0 in ].(yr - p),(yr + p).[
by XXREAL_1:4;
then
f . m0 in Ball (
yr,
p)
by A1, FRECHET:7;
then
f . m0 in { q where q is Element of RealSpace : dist (yr,q) < p }
by METRIC_1:def 14;
then consider q0 being
Element of
RealSpace such that A13:
f . m0 = q0
and A14:
dist (
yr,
q0)
< p
;
reconsider g2 =
yr as
Point of
RealSpace ;
ex
x1r,
y1r being
Real st
(
q0 = x1r &
g2 = y1r &
dist (
q0,
g2)
= real_dist . (
q0,
g2) &
dist (
q0,
g2)
= (Pitag_dist 1) . (
<*q0*>,
<*g2*>) &
dist (
q0,
g2)
= |.(x1r - y1r).| )
by Th6;
hence
|.((seq . m) - z).| < p
by A14, A1, A5, A13;
verum end; hence
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - z).| < p
;
verum end;
hence
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - z).| < p
;
verum
end;
hence
seq is convergent
by SEQ_2:def 6; ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) )
thus
ex z being Real st
( z in lim_f f & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - z).| < p ) )
by A3, A7; verum