let r be real number ; :: thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (c_n r) . n in NAT )
assume A1: (scf r) . 0 > 0 ; :: thesis: for n being Nat holds (c_n r) . n in NAT
set s1 = c_n r;
set s = scf r;
A2: (scf r) . 0 in NAT by A1, INT_1:16;
defpred S2[ Nat] means (c_n r) . $1 in NAT ;
A3: S2[ 0 ] by A2, Def6;
A4: S2[1]
proof
reconsider n1 = (scf r) . 1 as Element of NAT by Th38, INT_1:16;
reconsider n2 = (scf r) . 0 as Element of NAT by A1, INT_1:16;
(n1 * n2) + 1 in NAT ;
hence S2[1] by Def6; :: thesis: verum
end;
A5: 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 A6: ( (c_n r) . n in NAT & (c_n r) . (n + 1) in NAT ) ; :: thesis: S2[n + 2]
then reconsider n1 = (c_n r) . n as Element of NAT ;
reconsider n2 = (c_n r) . (n + 1) as Element of NAT by A6;
n + 2 >= 0 + 1 by XREAL_1:9;
then reconsider n3 = (scf r) . (n + 2) as Element of NAT by Th38, INT_1:16;
(n3 * n2) + n1 in NAT ;
hence S2[n + 2] by Def6; :: thesis: verum
end;
A7: for n being Nat holds S2[n] from FIB_NUM:sch 1(A3, A4, A5);
 let n be Nat; :: thesis: (c_n r) . n in NAT
thus (c_n r) . n in NAT by A7; :: thesis: verum