let r be real number ; :: thesis: ( (scf r) . 0 > 0 implies for n being Nat holds (c_n r) . n > 0 )
assume A1: (scf r) . 0 > 0 ; :: thesis: for n being Nat holds (c_n r) . n > 0
set s = scf r;
set s1 = c_n r;
A2: ( (c_n r) . 0 = (scf r) . 0 & (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0 )) + 1 ) by Def6;
defpred S2[ Nat] means (c_n r) . $1 > 0 ;
A3: S2[ 0 ] by A1, Def6;
(scf r) . 1 >= 0 by Th38;
then ((scf r) . 1) * ((scf r) . 0 ) >= 0 by A1;
then (c_n r) . 1 > 0 + 0 by A2;
then A4: S2[1] ;
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] )
n + 2 > 1 + 0 by XREAL_1:10;
then A6: (scf r) . (n + 2) >= 0 by Th38;
A7: (c_n r) . (n + 2) = (((scf r) . (n + 2)) * ((c_n r) . (n + 1))) + ((c_n r) . n) by Def6;
assume that
A8: (c_n r) . n > 0 and
A9: (c_n r) . (n + 1) > 0 ; :: thesis: S2[n + 2]
((scf r) . (n + 2)) * ((c_n r) . (n + 1)) >= 0 by A6, A9;
hence S2[n + 2] by A7, A8; :: thesis: verum
end;
A10: for n being Nat holds S2[n] from FIB_NUM:sch 1(A3, A4, A5);
 let n be Nat; :: thesis: (c_n r) . n > 0
thus (c_n r) . n > 0 by A10; :: thesis: verum