let r be Real; :: thesis: ( ( for n being Nat holds (scf r) . n <> 0 ) implies for n being Nat st n >= 1 holds
((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) )
set s1 = c_n r;
set s2 = c_d r;
set s = scf r;
defpred S₂[ Nat] means ((c_n r) . $1) / ((c_d r) . $1) = (((c_n r) . ($1 + 1)) - ((c_n r) . ($1 - 1))) / (((c_d r) . ($1 + 1)) - ((c_d r) . ($1 - 1)));
assume A1: for n being Nat holds (scf r) . n <> 0 ; :: thesis: for n being Nat st n >= 1 holds
((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1)))
A2: for n being Nat st n >= 1 & S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis: ( n >= 1 & S₂[n] implies S₂[n + 1] )
assume that
n >= 1 and
((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ; :: thesis: S₂[n + 1]
( ((((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n)) - ((c_n r) . n) = ((c_n r) . (n + 2)) - ((c_n r) . n) & ((c_d r) . (n + 2)) - ((c_d r) . n) = ((((scf r) . (n + 2)) * ((c_d r) . (n + 1))) + ((c_d r) . n)) - ((c_d r) . n) ) by Def5, Def6;
hence S₂[n + 1] by A1, XCMPLX_1:91; :: thesis: verum

end;

let n be Nat; :: thesis: ( n >= 1 implies ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) )
(((c_n r) . (1 + 1)) - ((c_n r) . (1 - 1))) / (((c_d r) . (1 + 1)) - ((c_d r) . (1 - 1))) = (((((scf r) . (2 + 0)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0)) - ((c_n r) . 0)) / (((c_d r) . (2 + 0)) - ((c_d r) . 0)) by Def5
.= (((((scf r) . 2) * ((c_n r) . 1)) + ((c_n r) . 0)) - ((c_n r) . 0)) / (((((scf r) . 2) * ((c_d r) . 1)) + ((c_d r) . 0)) - ((c_d r) . 0)) by Def6
.= ((c_n r) . 1) / ((c_d r) . 1) by A1, XCMPLX_1:91 ;
then A3: S₂[1] ;
for n being Nat st n >= 1 holds
S₂[n] from NAT_1:sch 8(A3, A2);
hence ( n >= 1 implies ((c_n r) . n) / ((c_d r) . n) = (((c_n r) . (n + 1)) - ((c_n r) . (n - 1))) / (((c_d r) . (n + 1)) - ((c_d r) . (n - 1))) ) ; :: thesis: verum