deffunc H₁( Nat) -> set = 1 / ($1 + 1);
consider s0 being Real_Sequence such that
A1: for n being Nat holds s0 . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Nat) -> set = 1 / (2 * ($1 + 1));
consider s1 being Real_Sequence such that
A2: for n being Nat holds s1 . n = H₂(n) from SEQ_1:sch 1();
deffunc H₃( Nat) -> set = 1 + (1 / (2 * ($1 + 1)));
consider s2 being Real_Sequence such that
A3: for n being Nat holds s2 . n = H₃(n) from SEQ_1:sch 1();
deffunc H₄( Nat) -> set = (s2 . $1) * PI;
consider s3 being Real_Sequence such that
A4: for n being Nat holds s3 . n = H₄(n) from SEQ_1:sch 1();
A5: for n being Nat holds s1 . n = (1 / 2) * (s0 . n)

proof

let n be Nat; :: thesis: s1 . n = (1 / 2) * (s0 . n)
s1 . n = 1 / (2 * (n + 1)) by A2
.= (1 / 2) * (1 / (n + 1)) by XCMPLX_1:102
.= (1 / 2) * (s0 . n) by A1 ;
hence s1 . n = (1 / 2) * (s0 . n) ; :: thesis: verum

end;

A6: ( s1 is convergent & lim s1 = 0 )

proof

A7: ( s0 is convergent & lim s0 = 0 ) by A1, SEQ_4:31;
then ( (1 / 2) (#) s0 is convergent & lim ((1 / 2) (#) s0) = (1 / 2) * (lim s0) ) by SEQ_2:8;
hence ( s1 is convergent & lim s1 = 0 ) by A7, A5, SEQ_1:9; :: thesis: verum

end;

reconsider s4 = seq_const 1 as convergent Real_Sequence ;
A8: dom ((seq_const 1) + s1) = NAT by FUNCT_2:def 1;
A9: for n being Nat holds s2 . n = ((seq_const 1) + s1) . n

proof

let n be Nat; :: thesis: s2 . n = ((seq_const 1) + s1) . n
s2 . n = 1 + (1 / (2 * (n + 1))) by A3
.= 1 + (s1 . n) by A2
.= ((seq_const 1) . n) + (s1 . n) by SEQ_1:57
.= ((seq_const 1) + s1) . n by A8, ORDINAL1:def 12, VALUED_1:def 1 ;
hence s2 . n = ((seq_const 1) + s1) . n ; :: thesis: verum

end;

A10: s2 = (seq_const 1) + s1 by A9;
then A11: lim s2 = (lim (seq_const 1)) + (lim s1) by A6, SEQ_2:6
.= 1 + 0 by A6 ;
A12: for n being Nat holds s3 . n <> 0

proof

let n be Nat; :: thesis: s3 . n <> 0
s3 . n = (s2 . n) * PI by A4
.= (1 + (1 / (2 * (n + 1)))) * PI by A3 ;
hence s3 . n <> 0 by Lm9; :: thesis: verum

end;

for n being Nat holds s3 . n = (PI (#) s2) . n

proof

let n be Nat; :: thesis: s3 . n = (PI (#) s2) . n
dom (PI (#) s2) = NAT by FUNCT_2:def 1;
then (PI (#) s2) . n = PI * (s2 . n) by ORDINAL1:def 12, VALUED_1:def 5
.= s3 . n by A4 ;
hence s3 . n = (PI (#) s2) . n ; :: thesis: verum

end;

then A15: s3 = PI (#) s2 ;
then A16: lim s3 = PI * (lim s2) by A10, A6, SEQ_2:8
.= PI by A11 ;
for n being Nat holds w_seq . n = (s3 ") . n

proof

let n be Nat; :: thesis: w_seq . n = (s3 ") . n
A17: s3 . n = (s2 . n) * PI by A4
.= (1 + (1 / (2 * (n + 1)))) * PI by A3 ;
(s3 . n) " = 1 / ((1 + (1 / (2 * (n + 1)))) * PI) by A17
.= w_seq . n by Def8 ;
hence w_seq . n = (s3 ") . n by VALUED_1:10; :: thesis: verum

end;

then w_seq = s3 " ;
hence ( w_seq is convergent & lim w_seq = 1 / PI ) by SEQ_2:21, SEQ_2:22, SEQ_1:5, A12, A10, A6, A15, A16, COMPTRIG:5; :: thesis: verum