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