let r be Real; :: thesis: for n being Nat holds (c_n r) . n is Integer
defpred S₁[ Nat] means (c_n r) . $1 is Integer;
A1: for n being Nat st S₁[n] & S₁[n + 1] holds
S₁[n + 2]

proof

let n be Nat; :: thesis: ( S₁[n] & S₁[n + 1] implies S₁[n + 2] )
assume that
A2: (c_n r) . n is Integer and
A3: (c_n r) . (n + 1) is Integer ; :: thesis: S₁[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 S₁[n + 2] by A2, A3; :: thesis: verum

end;

A5: S₁[1]

proof

(c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 by REAL_3:def 5;
hence S₁[1] ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

(c_n r) . 0 = (scf r) . 0 by REAL_3:def 5;
hence S₁[ 0 ] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from FIB_NUM:sch 1(A6, A5, A1);
hence for n being Nat holds (c_n r) . n is Integer ; :: thesis: verum