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)
A2: f . (x - h) = (x - h) ^2 by A1;
(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