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