let r be Real; :: thesis: for n being Nat holds (c_n r) . n is Integer
defpred S1[ Nat] means (c_n r) . $1 is Integer;
A1: for n being Nat st S1[n] & S1[n + 1] holds
S1[n + 2]
proof
let n be Nat; :: thesis: ( S1[n] & S1[n + 1] implies S1[n + 2] )
assume that
A2: (c_n r) . n is Integer and
A3: (c_n r) . (n + 1) is Integer ; :: thesis: S1[n + 2]
(c_n r) . (n + 2) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by REAL_3:def 5;
hence S1[n + 2] by A2, A3; :: thesis: verum
end;
A5: S1[1]
proof
(c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 by REAL_3:def 5;
hence S1[1] ; :: thesis: verum
end;
A6: S1[ 0 ]
proof
(c_n r) . 0 = (scf r) . 0 by REAL_3:def 5;
hence S1[ 0 ] ; :: thesis: verum
end;
for n being Nat holds S1[n] from FIB_NUM:sch 1(A6, A5, A1);
 hence for n being Nat holds (c_n r) . n is Integer ; :: thesis: verum