let a, b be Real; :: thesis: for n being Element of NAT st a * (n + 1) <> 0 holds
( (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL & ( for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ) )
let n be Element of NAT ; :: thesis: ( a * (n + 1) <> 0 implies ( (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL & ( for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ) ) )
assume A1: a * (n + 1) <> 0 ; :: thesis: ( (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL & ( for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ) )
A2: [#] REAL = dom ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) by FUNCT_2:def 1;
A3: [#] REAL = dom (AffineMap (a,b)) by FUNCT_2:def 1;
A4: for x being Real st x in REAL holds
(AffineMap (a,b)) . x = (a * x) + b by FCONT_1:def 4;
then A5: AffineMap (a,b) is_differentiable_on REAL by A3, FDIFF_1:23;
for x being Real holds (#Z (n + 1)) * (AffineMap (a,b)) is_differentiable_in x

proof

let x be Real; :: thesis: (#Z (n + 1)) * (AffineMap (a,b)) is_differentiable_in x
x in REAL by XREAL_0:def 1;
then AffineMap (a,b) is_differentiable_in x by A3, A5, FDIFF_1:9;
hence (#Z (n + 1)) * (AffineMap (a,b)) is_differentiable_in x by TAYLOR_1:3; :: thesis: verum

end;

then ( [#] REAL = dom ((#Z (n + 1)) * (AffineMap (a,b))) & ( for x being Real st x in REAL holds
(#Z (n + 1)) * (AffineMap (a,b)) is_differentiable_in x ) ) by FUNCT_2:def 1;
then A6: (#Z (n + 1)) * (AffineMap (a,b)) is_differentiable_on REAL by FDIFF_1:9;
hence (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL by A2, FDIFF_1:20; :: thesis: for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n
A7: for x being Real st x in REAL holds
(((#Z (n + 1)) * (AffineMap (a,b))) `| REAL) . x = (a * (n + 1)) * (((AffineMap (a,b)) . x) #Z n)

proof

set m = n + 1;
let x be Real; :: thesis: ( x in REAL implies (((#Z (n + 1)) * (AffineMap (a,b))) `| REAL) . x = (a * (n + 1)) * (((AffineMap (a,b)) . x) #Z n) )
assume A8: x in REAL ; :: thesis: (((#Z (n + 1)) * (AffineMap (a,b))) `| REAL) . x = (a * (n + 1)) * (((AffineMap (a,b)) . x) #Z n)
AffineMap (a,b) is_differentiable_in x by A3, A5, FDIFF_1:9, A8;
then diff (((#Z (n + 1)) * (AffineMap (a,b))),x) = ((n + 1) * (((AffineMap (a,b)) . x) #Z ((n + 1) - 1))) * (diff ((AffineMap (a,b)),x)) by TAYLOR_1:3
.= ((n + 1) * (((AffineMap (a,b)) . x) #Z ((n + 1) - 1))) * (((AffineMap (a,b)) `| REAL) . x) by A5, FDIFF_1:def 7, A8
.= ((n + 1) * (((AffineMap (a,b)) . x) #Z ((n + 1) - 1))) * a by A3, A4, FDIFF_1:23, A8 ;
hence (((#Z (n + 1)) * (AffineMap (a,b))) `| REAL) . x = (a * (n + 1)) * (((AffineMap (a,b)) . x) #Z n) by A6, FDIFF_1:def 7, A8; :: thesis: verum

end;

A9: for x being Real st x in REAL holds
(((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n

proof

let x be Real; :: thesis: ( x in REAL implies (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n )
assume A10: x in REAL ; :: thesis: (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n
(((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = (1 / (a * (n + 1))) * (diff (((#Z (n + 1)) * (AffineMap (a,b))),x)) by A2, A6, FDIFF_1:20, A10
.= (1 / (a * (n + 1))) * ((((#Z (n + 1)) * (AffineMap (a,b))) `| REAL) . x) by A6, FDIFF_1:def 7, A10
.= (1 / (a * (n + 1))) * ((a * (n + 1)) * (((AffineMap (a,b)) . x) #Z n)) by A7, A10
.= ((1 / (a * (n + 1))) * (a * (n + 1))) * (((AffineMap (a,b)) . x) #Z n)
.= ((a * (n + 1)) / (a * (n + 1))) * (((AffineMap (a,b)) . x) #Z n) by XCMPLX_1:99
.= 1 * (((AffineMap (a,b)) . x) #Z n) by A1, XCMPLX_1:60
.= ((a * x) + b) #Z n by FCONT_1:def 4 ;
hence (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ; :: thesis: verum

end;

let x be Real; :: thesis: (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n
x in REAL by XREAL_0:def 1;
hence (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n by A9; :: thesis: verum