A1: [#] REAL = dom (sin * (AffineMap 2,0 )) by FUNCT_2:def 1;
A2: for x being Real st x in REAL holds
(AffineMap 2,0 ) . x = (2 * x) + 0 by JORDAN16:def 3;
then A3: ( sin * (AffineMap 2,0 ) is_differentiable_on REAL & ( for x being Real st x in REAL holds
((sin * (AffineMap 2,0 )) `| REAL ) . x = 2 * (cos . ((2 * x) + 0 )) ) ) by A1, FDIFF_4:37;
for x being Real st x in REAL holds
(((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = cos (2 * x)

proof

let x be Real; :: thesis: ( x in REAL implies (((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = cos (2 * x) )
assume x in REAL ; :: thesis: (((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = cos (2 * x)
(((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = (1 / 2) * (diff (sin * (AffineMap 2,0 )),x) by Lm4, A3, FDIFF_1:28
.= (1 / 2) * (((sin * (AffineMap 2,0 )) `| REAL ) . x) by A3, FDIFF_1:def 8
.= (1 / 2) * (2 * (cos . ((2 * x) + 0 ))) by A1, A2, FDIFF_4:37
.= cos (2 * x) ;
hence (((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = cos (2 * x) ; :: thesis: verum

end;

hence ( (1 / 2) (#) (sin * (AffineMap 2,0 )) is_differentiable_on REAL & ( for x being Real holds (((1 / 2) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = cos (2 * x) ) ) by Lm4, A3, FDIFF_1:28; :: thesis: verum