let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ) iff Rseq is convergent_in_cod1 )

hereby :: thesis: ( Rseq is convergent_in_cod1 implies for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} )

assume A13:
Rseq is convergent_in_cod1
; :: thesis: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} assume A1:
for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
; :: thesis: Rseq is convergent_in_cod1

end;now :: thesis: for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent

hence
Rseq is convergent_in_cod1
; :: thesis: verumlet m be Element of NAT ; :: thesis: ProjMap2 (Rseq,m) is convergent

not lim_filter ((ProjMap2 ((# Rseq),m)),(Frechet_Filter NAT)) is empty by A1;

then consider r being Element of (TopSpaceMetr RealSpace) such that

A2: r in lim_filter ((ProjMap2 ((# Rseq),m)),(Frechet_Filter NAT)) ;

A3: r in lim_f (ProjMap2 ((# Rseq),m)) by A2;

A4: Balls r is basis of (BOOL2F (NeighborhoodSystem r)) by CARDFIL3:6;

reconsider r1 = r as Real ;

end;not lim_filter ((ProjMap2 ((# Rseq),m)),(Frechet_Filter NAT)) is empty by A1;

then consider r being Element of (TopSpaceMetr RealSpace) such that

A2: r in lim_filter ((ProjMap2 ((# Rseq),m)),(Frechet_Filter NAT)) ;

A3: r in lim_f (ProjMap2 ((# Rseq),m)) by A2;

A4: Balls r is basis of (BOOL2F (NeighborhoodSystem r)) by CARDFIL3:6;

reconsider r1 = r as Real ;

now :: thesis: for e being Real st 0 < e holds

ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

hence
ProjMap2 (Rseq,m) is convergent
by SEQ_2:def 6; :: thesis: verumex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e )

assume 0 < e ; :: thesis: ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

then consider m1 being Nat such that

A5: not m1 is zero and

A6: 1 / m1 < e by Th5;

consider y being Point of RealSpace such that

A7: y = r and

A8: Balls r = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

A9: Ball (y,(1 / m1)) c= Ball (y,e) by A6, PCOMPS_1:1;

Ball (y,(1 / m1)) in Balls r by A8, A5;

then consider i being Nat such that

A10: for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),m)) . j in Ball (y,(1 / m1)) by A4, A3, CARDFIL2:97;

thus ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e :: thesis: verum

end;for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e )

assume 0 < e ; :: thesis: ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

then consider m1 being Nat such that

A5: not m1 is zero and

A6: 1 / m1 < e by Th5;

consider y being Point of RealSpace such that

A7: y = r and

A8: Balls r = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

A9: Ball (y,(1 / m1)) c= Ball (y,e) by A6, PCOMPS_1:1;

Ball (y,(1 / m1)) in Balls r by A8, A5;

then consider i being Nat such that

A10: for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),m)) . j in Ball (y,(1 / m1)) by A4, A3, CARDFIL2:97;

thus ex N being Nat st

for n being Nat st N <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e :: thesis: verum

proof

take
i
; :: thesis: for n being Nat st i <= n holds

|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

let j be Nat; :: thesis: ( i <= j implies |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e )

assume i <= j ; :: thesis: |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e

then (ProjMap2 ((# Rseq),m)) . j in Ball (y,e) by A9, A10;

then (ProjMap2 ((# Rseq),m)) . j in ].(y - e),(y + e).[ by FRECHET:7;

hence |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e by A7, FCONT_3:1; :: thesis: verum

end;|.(((ProjMap2 (Rseq,m)) . n) - r1).| < e

let j be Nat; :: thesis: ( i <= j implies |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e )

assume i <= j ; :: thesis: |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e

then (ProjMap2 ((# Rseq),m)) . j in Ball (y,e) by A9, A10;

then (ProjMap2 ((# Rseq),m)) . j in ].(y - e),(y + e).[ by FRECHET:7;

hence |.(((ProjMap2 (Rseq,m)) . j) - r1).| < e by A7, FCONT_3:1; :: thesis: verum

now :: thesis: for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}

hence
for x being Element of NAT holds lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}
; :: thesis: verumlet x be Element of NAT ; :: thesis: lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {}

consider r being Real such that

A14: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((ProjMap2 (Rseq,x)) . m) - r).| < p by A13, SEQ_2:def 6;

reconsider r1 = r as Point of (TopSpaceMetr RealSpace) by XREAL_0:def 1;

A15: Balls r1 is basis of (BOOL2F (NeighborhoodSystem r1)) by CARDFIL3:6;

for b being Element of Balls r1 ex i being Nat st

for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

hence lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: verum

end;consider r being Real such that

A14: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((ProjMap2 (Rseq,x)) . m) - r).| < p by A13, SEQ_2:def 6;

reconsider r1 = r as Point of (TopSpaceMetr RealSpace) by XREAL_0:def 1;

A15: Balls r1 is basis of (BOOL2F (NeighborhoodSystem r1)) by CARDFIL3:6;

for b being Element of Balls r1 ex i being Nat st

for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

proof

then
lim_f (ProjMap2 ((# Rseq),x)) <> {}
by A15, CARDFIL2:97;
let b be Element of Balls r1; :: thesis: ex i being Nat st

for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

consider y being Point of RealSpace such that

A16: y = r1 and

A17: Balls r1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

b in { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by A17;

then consider n0 being Nat such that

A18: b = Ball (y,(1 / n0)) and

A19: n0 <> 0 ;

( 0 < n0 & 0 * n0 < 1 ) by A19;

then consider n1 being Nat such that

A20: for m being Nat st n1 <= m holds

|.(((ProjMap2 (Rseq,x)) . m) - r).| < 1 / n0 by A14, XREAL_1:81;

for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b ; :: thesis: verum

end;for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

consider y being Point of RealSpace such that

A16: y = r1 and

A17: Balls r1 = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;

b in { (Ball (y,(1 / n))) where n is Nat : n <> 0 } by A17;

then consider n0 being Nat such that

A18: b = Ball (y,(1 / n0)) and

A19: n0 <> 0 ;

( 0 < n0 & 0 * n0 < 1 ) by A19;

then consider n1 being Nat such that

A20: for m being Nat st n1 <= m holds

|.(((ProjMap2 (Rseq,x)) . m) - r).| < 1 / n0 by A14, XREAL_1:81;

now :: thesis: ex n1 being Nat st

for j being Nat st n1 <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

hence
ex i being Nat st for j being Nat st n1 <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

take n1 = n1; :: thesis: for j being Nat st n1 <= j holds

(ProjMap2 ((# Rseq),x)) . j in b

end;(ProjMap2 ((# Rseq),x)) . j in b

hereby :: thesis: verum

let j be Nat; :: thesis: ( n1 <= j implies (ProjMap2 ((# Rseq),x)) . j in b )

assume n1 <= j ; :: thesis: (ProjMap2 ((# Rseq),x)) . j in b

then A21: |.(((ProjMap2 (Rseq,x)) . j) - r).| < 1 / n0 by A20;

(ProjMap2 (Rseq,x)) . j = r + (((ProjMap2 (Rseq,x)) . j) - r) ;

then (ProjMap2 (Rseq,x)) . j in ].(r - (1 / n0)),(r + (1 / n0)).[ by A21, FCONT_3:3;

hence (ProjMap2 ((# Rseq),x)) . j in b by A16, A18, FRECHET:7; :: thesis: verum

end;assume n1 <= j ; :: thesis: (ProjMap2 ((# Rseq),x)) . j in b

then A21: |.(((ProjMap2 (Rseq,x)) . j) - r).| < 1 / n0 by A20;

(ProjMap2 (Rseq,x)) . j = r + (((ProjMap2 (Rseq,x)) . j) - r) ;

then (ProjMap2 (Rseq,x)) . j in ].(r - (1 / n0)),(r + (1 / n0)).[ by A21, FCONT_3:3;

hence (ProjMap2 ((# Rseq),x)) . j in b by A16, A18, FRECHET:7; :: thesis: verum

for j being Nat st i <= j holds

(ProjMap2 ((# Rseq),x)) . j in b ; :: thesis: verum

hence lim_filter ((ProjMap2 ((# Rseq),x)),(Frechet_Filter NAT)) <> {} ; :: thesis: verum