theorem :: DIFF_2:25

for h, a, b, x being Real holds (bD ((AffineMap (a,b)),h)) . x = a * h