let h, x 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 Th22
.= (((cdif (f,h)) . 1) . x) / h by Th16 ;
hence [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif (f,h)) . 1) . x) / h ; :: thesis: verum