let a, b be Real; 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 ; ( 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 ) ) )
A1:
[#] REAL = dom ((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b)))
by FUNCT_2:def 1;
A2:
[#] REAL = dom (AffineMap a,b)
by FUNCT_2:def 1;
A3:
for x being Real st x in REAL holds
(AffineMap a,b) . x = (a * x) + b
by JORDAN16:def 3;
then A4:
AffineMap a,b is_differentiable_on REAL
by A2, FDIFF_1:31;
for x being Real holds (#Z (n + 1)) * (AffineMap a,b) is_differentiable_in x
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 A5:
(#Z (n + 1)) * (AffineMap a,b) is_differentiable_on REAL
by FDIFF_1:16;
A6:
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;
( x in REAL implies (((#Z (n + 1)) * (AffineMap a,b)) `| REAL ) . x = (a * (n + 1)) * (((AffineMap a,b) . x) #Z n) )
assume
x in REAL
;
(((#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 A2, A4, FDIFF_1:16;
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 A4, FDIFF_1:def 8
.=
((n + 1) * (((AffineMap a,b) . x) #Z ((n + 1) - 1))) * a
by A2, A3, FDIFF_1:31
;
hence
(((#Z (n + 1)) * (AffineMap a,b)) `| REAL ) . x = (a * (n + 1)) * (((AffineMap a,b) . x) #Z n)
by A5, FDIFF_1:def 8;
verum
end;
assume A7:
a * (n + 1) <> 0
; ( (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 ) )
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;
( x in REAL implies (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) `| REAL ) . x = ((a * x) + b) #Z n )
assume
x in REAL
;
(((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 A1, A5, FDIFF_1:28
.=
(1 / (a * (n + 1))) * ((((#Z (n + 1)) * (AffineMap a,b)) `| REAL ) . x)
by A5, FDIFF_1:def 8
.=
(1 / (a * (n + 1))) * ((a * (n + 1)) * (((AffineMap a,b) . x) #Z n))
by A6
.=
((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:100
.=
1
* (((AffineMap a,b) . x) #Z n)
by A7, XCMPLX_1:60
.=
((a * x) + b) #Z n
by JORDAN16:def 3
;
hence
(((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap a,b))) `| REAL ) . x = ((a * x) + b) #Z n
;
verum
end;
hence
( (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 ) )
by A1, A5, FDIFF_1:28; verum