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

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