let h, x be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(cD (f,h)) . x = (2 * h) * x
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = x ^2 ) implies (cD (f,h)) . x = (2 * h) * x )
assume A1: for x being Real holds f . x = x ^2 ; :: thesis: (cD (f,h)) . x = (2 * h) * x
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= ((x + (h / 2)) ^2) - (f . (x - (h / 2))) by A1
.= ((x + (h / 2)) ^2) - ((x - (h / 2)) ^2) by A1
.= h * (2 * x) ;
hence (cD (f,h)) . x = (2 * h) * x ; :: thesis: verum