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