let k be Nat; :: thesis: ( bseq k is convergent & lim (bseq k) = 1 / (k !) & lim (bseq k) = eseq . k )
defpred S₁[ Nat] means ( bseq $1 is convergent & lim (bseq $1) = 1 / ($1 !) );

A1: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

deffunc H₁( Nat) -> set = (1 / (k + 1)) * ((bseq k) . $1);
consider seq being Real_Sequence such that
A3: for n being Nat holds seq . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Nat) -> set = (seq . $1) * ((aseq k) . $1);
consider seq1 being Real_Sequence such that
A4: for n being Nat holds seq1 . n = H₂(n) from SEQ_1:sch 1();
A5: for n being Nat st n >= 1 holds
(bseq (k + 1)) . n = seq1 . n

proof

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;

A6: seq = (1 / (k + 1)) (#) (bseq k) by A3, SEQ_1:9;
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;

end;

A12: S₁[ 0 ]

proof

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

proof

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;

hence bseq 0 is convergent by SEQ_4:18; :: thesis: lim (bseq 0) = 1 / (0 !)
lim (seq_const 1) = 1 by A13, Th9;
hence lim (bseq 0) = 1 / (0 !) by A14, NEWTON:12, SEQ_4:19; :: thesis: verum

end;

for k being Nat holds S₁[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