let x, h be Real; :: thesis: for f being Function of REAL ,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif f,h) . 1) . x) / h
let f be Function of REAL ,REAL ; :: thesis: [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif f,h) . 1) . x) / h
[!f,(x - (h / 2)),(x + (h / 2))!] = ((cD f,h) . x) / h by Th29
.= (((cdif f,h) . 1) . x) / h by Th23 ;
hence [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif f,h) . 1) . x) / h ; :: thesis: verum