let h be Real; :: thesis: for f being Function of REAL,REAL

for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

let f be Function of REAL,REAL; :: thesis: for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

defpred S_{1}[ Nat] means (cdif (f,h)) . $1 is Function of REAL,REAL;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Def8;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A2, A1);

hence for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL ; :: thesis: verum

for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

let f be Function of REAL,REAL; :: thesis: for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL

defpred S

A1: for k being Nat st S

S

proof

A2:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume (cdif (f,h)) . k is Function of REAL,REAL ; :: thesis: S_{1}[k + 1]

then cD (((cdif (f,h)) . k),h) is Function of REAL,REAL ;

hence S_{1}[k + 1]
by Def8; :: thesis: verum

end;assume (cdif (f,h)) . k is Function of REAL,REAL ; :: thesis: S

then cD (((cdif (f,h)) . k),h) is Function of REAL,REAL ;

hence S

for n being Nat holds S

hence for n being Nat holds (cdif (f,h)) . n is Function of REAL,REAL ; :: thesis: verum