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 ) ) )
assume A1:
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 ) )
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
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; 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;
( 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
;
(((#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;
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;
( 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
;
(((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
;
verum
end;
let x be Real; (((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; verum