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