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: now

let k be Element of 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₁( Element of NAT ) -> Element of COMPLEX = (1 / (k + 1)) * ((bseq k) . $1);
consider seq being Real_Sequence such that
A3: for n being Element of NAT holds seq . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Element of NAT ) -> set = (seq . $1) * ((aseq k) . $1);
consider seq1 being Real_Sequence such that
A4: for n being Element of NAT holds seq1 . n = H₂(n) from SEQ_1:sch 1();
A5: 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 A3
.= seq1 . n by A4 ;
:: thesis: verum

end;

A6: seq = (1 / (k + 1)) (#) (bseq k) by A3, SEQ_1:13;
then A7: seq is convergent by A2, SEQ_2:21;
A8: lim seq = (1 / (k + 1)) * (1 / (k ! )) by A2, A6, SEQ_2:22
.= 1 / ((k + 1) ! ) by Th12 ;
A9: aseq k is convergent by Th9;
A10: seq1 = seq (#) (aseq k) by A4, SEQ_1:12;
then A11: seq1 is convergent by A7, A9, SEQ_2:28;
hence bseq (k + 1) is convergent by A5, SEQ_4:31; :: thesis: lim (bseq (k + 1)) = 1 / ((k + 1) ! )
lim seq1 = (lim seq) * (lim (aseq k)) by A7, A10, A9, SEQ_2:29
.= 1 / ((k + 1) ! ) by A8, Th9 ;
hence lim (bseq (k + 1)) = 1 / ((k + 1) ! ) by A11, A5, SEQ_4:32; :: thesis: verum

end;

end;

A12: S₁[ 0 ]

proof

reconsider bseq0 = NAT --> 1 as Real_Sequence by FUNCOP_1:57;
A13: 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 A14: bseq0 is convergent by Th10;
A15: 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 A14, SEQ_4:31; :: thesis: lim (bseq 0 ) = 1 / (0 ! )
lim bseq0 = 1 by A13, Th10;
hence lim (bseq 0 ) = 1 / (0 ! ) by A14, A15, NEWTON:18, SEQ_4:32; :: thesis: verum

end;

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