let k be Element of 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: S₁[ 0 ]

proof

reconsider bseq0 = NAT --> 1 as Real_Sequence by FUNCOP_1:57;
for n being Nat holds bseq0 . n = 1

proof

let n be Nat; :: thesis: bseq0 . n = 1
n in NAT by ORDINAL1:def 13;
hence bseq0 . n = 1 by FUNCOP_1:13; :: thesis: verum

end;

then A2: ( bseq0 is convergent & lim bseq0 = 1 ) by Th10;
A3: for n being Element of NAT st n >= 1 holds
(bseq 0 ) . n = bseq0 . n

proof

let n be Element of NAT ; :: thesis: ( n >= 1 implies (bseq 0 ) . n = bseq0 . n )
assume n >= 1 ; :: thesis: (bseq 0 ) . n = bseq0 . n
thus (bseq 0 ) . n = 1 by Th11
.= bseq0 . n by FUNCOP_1:13 ; :: thesis: verum

end;

hence bseq 0 is convergent by A2, SEQ_4:31; :: thesis: lim (bseq 0 ) = 1 / (0 ! )
thus lim (bseq 0 ) = 1 / (0 ! ) by A2, A3, NEWTON:18, SEQ_4:32; :: thesis: verum

end;

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

deffunc H₁( Element of NAT ) -> Element of K45() = (1 / (k + 1)) * ((bseq k) . $1);
consider seq being Real_Sequence such that
A6: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
A7: seq = (1 / (k + 1)) (#) (bseq k) by A6, SEQ_1:13;
A8: ( seq is convergent & lim seq = 1 / ((k + 1) ! ) )

proof

thus seq is convergent by A5, A7, SEQ_2:21; :: thesis: lim seq = 1 / ((k + 1) ! )
thus lim seq = (1 / (k + 1)) * (1 / (k ! )) by A5, A7, SEQ_2:22
.= 1 / ((k + 1) ! ) by Th12 ; :: thesis: verum

end;

deffunc H₂( Element of NAT ) -> set = (seq . $1) * ((aseq k) . $1);
consider seq1 being Real_Sequence such that
A9: for n being Element of NAT holds seq1 . n = H₂(n) from SEQ_1:sch 1();
A10: seq1 = seq (#) (aseq k) by A9, SEQ_1:12;
A11: ( seq1 is convergent & lim seq1 = 1 / ((k + 1) ! ) )

proof

A12: ( aseq k is convergent & lim (aseq k) = 1 ) by Th9;
hence seq1 is convergent by A8, A10, SEQ_2:28; :: thesis: lim seq1 = 1 / ((k + 1) ! )
thus lim seq1 = (lim seq) * (lim (aseq k)) by A8, A10, A12, SEQ_2:29
.= 1 / ((k + 1) ! ) by A8, A12 ; :: thesis: verum

end;

A13: for n being Element of NAT st n >= 1 holds
(bseq (k + 1)) . n = seq1 . n

proof

let n be Element of 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 Th7
.= (seq . n) * ((aseq k) . n) by A6
.= seq1 . n by A9 ;
:: thesis: verum

end;

hence bseq (k + 1) is convergent by A11, SEQ_4:31; :: thesis: lim (bseq (k + 1)) = 1 / ((k + 1) ! )
thus lim (bseq (k + 1)) = 1 / ((k + 1) ! ) by A11, A13, SEQ_4:32; :: thesis: verum

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A4);
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