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)
then f . (x + h) = (x + h) ^2 ;
then (fD (f,h)) . x = ((x + h) ^2) - (f . x) by 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