let a, b be Real; :: thesis: ( AffineMap (a,b) is_differentiable_on REAL & ( for x being Real holds diff ((AffineMap (a,b)),x) = a ) )
reconsider Z = [#] REAL as open Subset of REAL ;
A1: dom (AffineMap (a,b)) = REAL by FUNCT_2:def 1;
A2: for x being Real st x in Z holds
(AffineMap (a,b)) . x = (a * x) + b by FCONT_1:def 4;
hence Ka: AffineMap (a,b) is_differentiable_on REAL by A1, FDIFF_1:23; :: thesis: for x being Real holds diff ((AffineMap (a,b)),x) = a
let x be Real; :: thesis: diff ((AffineMap (a,b)),x) = a
AC: x in Z by XREAL_0:def 1;
((AffineMap (a,b)) `| Z) . x = a by A1, A2, FDIFF_1:23, XREAL_0:def 1;
hence diff ((AffineMap (a,b)),x) = a by AC, FDIFF_1:def 7, Ka; :: thesis: verum