let r be real number ; :: thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) )
set s1 = c_n r;
set s = scf r;
defpred S₂[ Nat] means (bcf r) . ($1 + 1) = ((c_n r) . ($1 + 1)) / ((c_n r) . $1);
set s3 = bcf r;
assume A1: (scf r) . 0 > 0 ; :: thesis: for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n)
A2: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A3: (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) ; :: thesis: S₂[n + 1]
A4: (c_n r) . (n + 1) > 0 by A1, Th45;
(bcf r) . ((n + 1) + 1) = (1 / ((bcf r) . (n + 1))) + ((scf r) . ((n + 1) + 1)) by Def9
.= (((c_n r) . n) / ((c_n r) . (n + 1))) + ((scf r) . ((n + 1) + 1)) by A3, XCMPLX_1:57
.= (((c_n r) . n) + (((scf r) . (n + 2)) * ((c_n r) . (n + 1)))) / ((c_n r) . (n + 1)) by A4, XCMPLX_1:113
.= ((c_n r) . (n + 2)) / ((c_n r) . (n + 1)) by Def6 ;
hence S₂[n + 1] ; :: thesis: verum

end;

(bcf r) . (0 + 1) = (1 / ((bcf r) . 0)) + ((scf r) . (0 + 1)) by Def9
.= (1 / ((scf r) . 0)) + ((scf r) . 1) by Def9
.= (1 + (((scf r) . 0) * ((scf r) . 1))) / ((scf r) . 0) by A1, XCMPLX_1:113
.= ((c_n r) . 1) / ((scf r) . 0) by Def6
.= ((c_n r) . (0 + 1)) / ((c_n r) . 0) by Def6 ;
then A5: S₂[ 0 ] ;
for n being Nat holds S₂[n] from NAT_1:sch 2(A5, A2);
hence for n being Nat holds (bcf r) . (n + 1) = ((c_n r) . (n + 1)) / ((c_n r) . n) ; :: thesis: verum