let r be real number ; ( ( for n being Nat holds (c_d r) . n <> 0 ) implies for n being Nat holds abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n))) )
set s1 = c_n r;
set s2 = c_d r;
assume A1:
for n being Nat holds (c_d r) . n <> 0
; for n being Nat holds abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
let n be Nat; abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
reconsider n = n as Element of NAT by ORDINAL1:def 12;
abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) =
abs (((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)))
by A1, Th65
.=
(abs ((- 1) |^ n)) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
by COMPLEX1:67
.=
(abs ((- 1) to_power n)) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
by POWER:41
.=
((abs (- 1)) to_power n) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
by SERIES_1:2
.=
((- (- 1)) to_power n) / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
by ABSVALUE:def 1
.=
1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
by POWER:26
;
hence
abs ((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))) = 1 / (abs (((c_d r) . (n + 1)) * ((c_d r) . n)))
; verum