let h, a, b, x be Real; :: thesis: (fD ((AffineMap (a,b)),h)) . x = a * h
(fD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . (x + h)) - ((AffineMap (a,b)) . x) by DIFF_1:3
.= ((a * (x + h)) + b) - ((AffineMap (a,b)) . x) by FCONT_1:def 4
.= (((a * x) + (a * h)) + b) - ((a * x) + b) by FCONT_1:def 4 ;
hence (fD ((AffineMap (a,b)),h)) . x = a * h ; :: thesis: verum