let n be Nat; :: thesis: for r being Real holds (c_d r) . n in NAT
let r be Real; :: thesis: (c_d r) . n in NAT
set s = scf r;
set s2 = c_d r;
defpred S2[ Nat] means (c_d r) . $1 in NAT ;
(c_d r) . 0 = 1 by Def6;
then A1: S2[ 0 ] ;
A2: for n being Nat st S2[n] & S2[n + 1] holds
S2[n + 2]
proof
let n be Nat; :: thesis: ( S2[n] & S2[n + 1] implies S2[n + 2] )
assume that
A3: (c_d r) . n in NAT and
A4: (c_d r) . (n + 1) in NAT ; :: thesis: S2[n + 2]
reconsider n2 = (c_d r) . (n + 1) as Element of NAT by A4;
reconsider n1 = (c_d r) . n as Element of NAT by A3;
n + 2 >= 0 + 1 by XREAL_1:7;
then reconsider n3 = (scf r) . (n + 2) as Element of NAT by Th38, INT_1:3;
(n3 * n2) + n1 in NAT ;
hence S2[n + 2] by Def6; :: thesis: verum
end;
(c_d r) . 1 = (scf r) . 1 by Def6;
then A5: S2[1] by Th38, INT_1:3;
for n being Nat holds S2[n] from FIB_NUM:sch 1(A1, A5, A2);
 hence (c_d r) . n in NAT ; :: thesis: verum