A1:
[#] REAL = dom (exp_R * (AffineMap 2,0 ))
by FUNCT_2:def 1;
A2:
[#] REAL = dom (AffineMap 2,0 )
by FUNCT_2:def 1;
A3:
for x being Real st x in REAL holds
(AffineMap 2,0 ) . x = (2 * x) + 0
by JORDAN16:def 3;
then A4:
( AffineMap 2,0 is_differentiable_on REAL & ( for x being Real st x in [#] REAL holds
((AffineMap 2,0 ) `| REAL ) . x = 2 ) )
by A2, FDIFF_1:31;
for x being Real st x in REAL holds
exp_R * (AffineMap 2,0 ) is_differentiable_in x
then A5:
exp_R * (AffineMap 2,0 ) is_differentiable_on REAL
by A1, FDIFF_1:16;
for x being Real st x in REAL holds
(((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x = (exp_R * (AffineMap 2,0 )) . x
proof
let x be
Real;
:: thesis: ( x in REAL implies (((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x = (exp_R * (AffineMap 2,0 )) . x )
assume
x in REAL
;
:: thesis: (((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x = (exp_R * (AffineMap 2,0 )) . x
A6:
AffineMap 2,
0 is_differentiable_in x
by A4, FDIFF_1:16;
(((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x =
(1 / 2) * (diff (exp_R * (AffineMap 2,0 )),x)
by Lm2, A5, FDIFF_1:28
.=
(1 / 2) * ((exp_R . ((AffineMap 2,0 ) . x)) * (diff (AffineMap 2,0 ),x))
by A6, TAYLOR_1:19
.=
(1 / 2) * ((exp_R . ((AffineMap 2,0 ) . x)) * (((AffineMap 2,0 ) `| REAL ) . x))
by A4, FDIFF_1:def 8
.=
(1 / 2) * ((exp_R . ((AffineMap 2,0 ) . x)) * 2)
by A2, A3, FDIFF_1:31
.=
(exp_R * (AffineMap 2,0 )) . x
by A1, FUNCT_1:22
;
hence
(((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x = (exp_R * (AffineMap 2,0 )) . x
;
:: thesis: verum
end;
hence
( (1 / 2) (#) (exp_R * (AffineMap 2,0 )) is_differentiable_on REAL & ( for x being Real holds (((1 / 2) (#) (exp_R * (AffineMap 2,0 ))) `| REAL ) . x = (exp_R * (AffineMap 2,0 )) . x ) )
by A5, Lm2, FDIFF_1:28; :: thesis: verum