let k be Nat; :: thesis: ( bseq k is convergent & lim (bseq k) = 1 / (k !) & lim (bseq k) = eseq . k )

defpred S_{1}[ Nat] means ( bseq $1 is convergent & lim (bseq $1) = 1 / ($1 !) );

_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A12, A1);

hence ( bseq k is convergent & lim (bseq k) = 1 / (k !) ) ; :: thesis: lim (bseq k) = eseq . k

hence lim (bseq k) = eseq . k by Def5; :: thesis: verum

defpred S

A1: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A12:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A2: S

thus S

proof

deffunc H_{1}( Nat) -> set = (1 / (k + 1)) * ((bseq k) . $1);

consider seq being Real_Sequence such that

A3: for n being Nat holds seq . n = H_{1}(n)
from SEQ_1:sch 1();

deffunc H_{2}( Nat) -> set = (seq . $1) * ((aseq k) . $1);

consider seq1 being Real_Sequence such that

A4: for n being Nat holds seq1 . n = H_{2}(n)
from SEQ_1:sch 1();

A5: for n being Nat st n >= 1 holds

(bseq (k + 1)) . n = seq1 . n

then A7: seq is convergent by A2;

A8: lim seq = (1 / (k + 1)) * (1 / (k !)) by A2, A6, SEQ_2:8

.= 1 / ((k + 1) !) by Th11 ;

A9: aseq k is convergent by Th8;

A10: seq1 = seq (#) (aseq k) by A4, SEQ_1:8;

then A11: seq1 is convergent by A7, A9;

hence bseq (k + 1) is convergent by A5, SEQ_4:18; :: thesis: lim (bseq (k + 1)) = 1 / ((k + 1) !)

lim seq1 = (lim seq) * (lim (aseq k)) by A7, A10, A9, SEQ_2:15

.= 1 / ((k + 1) !) by A8, Th8 ;

hence lim (bseq (k + 1)) = 1 / ((k + 1) !) by A11, A5, SEQ_4:19; :: thesis: verum

end;consider seq being Real_Sequence such that

A3: for n being Nat holds seq . n = H

deffunc H

consider seq1 being Real_Sequence such that

A4: for n being Nat holds seq1 . n = H

A5: for n being Nat st n >= 1 holds

(bseq (k + 1)) . n = seq1 . n

proof

A6:
seq = (1 / (k + 1)) (#) (bseq k)
by A3, SEQ_1:9;
let n be Nat; :: thesis: ( n >= 1 implies (bseq (k + 1)) . n = seq1 . n )

assume n >= 1 ; :: thesis: (bseq (k + 1)) . n = seq1 . n

hence (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by Th6

.= (seq . n) * ((aseq k) . n) by A3

.= seq1 . n by A4 ;

:: thesis: verum

end;assume n >= 1 ; :: thesis: (bseq (k + 1)) . n = seq1 . n

hence (bseq (k + 1)) . n = ((1 / (k + 1)) * ((bseq k) . n)) * ((aseq k) . n) by Th6

.= (seq . n) * ((aseq k) . n) by A3

.= seq1 . n by A4 ;

:: thesis: verum

then A7: seq is convergent by A2;

A8: lim seq = (1 / (k + 1)) * (1 / (k !)) by A2, A6, SEQ_2:8

.= 1 / ((k + 1) !) by Th11 ;

A9: aseq k is convergent by Th8;

A10: seq1 = seq (#) (aseq k) by A4, SEQ_1:8;

then A11: seq1 is convergent by A7, A9;

hence bseq (k + 1) is convergent by A5, SEQ_4:18; :: thesis: lim (bseq (k + 1)) = 1 / ((k + 1) !)

lim seq1 = (lim seq) * (lim (aseq k)) by A7, A10, A9, SEQ_2:15

.= 1 / ((k + 1) !) by A8, Th8 ;

hence lim (bseq (k + 1)) = 1 / ((k + 1) !) by A11, A5, SEQ_4:19; :: thesis: verum

proof

for k being Nat holds S
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

set bseq0 = seq_const 1;

A13: for n being Nat holds (seq_const 1) . n = 1 by SEQ_1:57;

A14: for n being Nat st n >= 1 holds

(bseq 0) . n = (seq_const 1) . n

lim (seq_const 1) = 1 by A13, Th9;

hence lim (bseq 0) = 1 / (0 !) by A14, NEWTON:12, SEQ_4:19; :: thesis: verum

end;set bseq0 = seq_const 1;

A13: for n being Nat holds (seq_const 1) . n = 1 by SEQ_1:57;

A14: for n being Nat st n >= 1 holds

(bseq 0) . n = (seq_const 1) . n

proof

hence
bseq 0 is convergent
by SEQ_4:18; :: thesis: lim (bseq 0) = 1 / (0 !)
let n be Nat; :: thesis: ( n >= 1 implies (bseq 0) . n = (seq_const 1) . n )

assume n >= 1 ; :: thesis: (bseq 0) . n = (seq_const 1) . n

thus (bseq 0) . n = 1 by Th10

.= (seq_const 1) . n by SEQ_1:57 ; :: thesis: verum

end;assume n >= 1 ; :: thesis: (bseq 0) . n = (seq_const 1) . n

thus (bseq 0) . n = 1 by Th10

.= (seq_const 1) . n by SEQ_1:57 ; :: thesis: verum

lim (seq_const 1) = 1 by A13, Th9;

hence lim (bseq 0) = 1 / (0 !) by A14, NEWTON:12, SEQ_4:19; :: thesis: verum

hence ( bseq k is convergent & lim (bseq k) = 1 / (k !) ) ; :: thesis: lim (bseq k) = eseq . k

hence lim (bseq k) = eseq . k by Def5; :: thesis: verum