theorem LemmaAffine: :: FUZIMPL2:2
for a, b being Real holds
( AffineMap (a,b) is_differentiable_on REAL & ( for x being Real holds diff ((AffineMap (a,b)),x) = a ) )