A1: for x being Real st x in REAL holds
(AffineMap 2,0 ) . x = (2 * x) + 0 by JORDAN16:def 3;
then A2: sin * (AffineMap 2,0 ) is_differentiable_on REAL by Lm2, FDIFF_4:37;
then A3: (1 / 4) (#) (sin * (AffineMap 2,0 )) is_differentiable_on REAL by Lm3, FDIFF_1:28;
A4: dom ((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) = [#] REAL by FUNCT_2:def 1;
A5: for x being Real st x in REAL holds
(AffineMap (1 / 2),0 ) . x = ((1 / 2) * x) + 0 by JORDAN16:def 3;
then A6: AffineMap (1 / 2),0 is_differentiable_on REAL by Lm1, FDIFF_1:31;
A7: for x being Real st x in REAL holds
(((1 / 4) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x = (1 / 2) * (cos (2 * x))

proof

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

end;

for x being Real st x in REAL holds
(((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) . x = (cos . x) ^2

proof

let x be Real; :: thesis: ( x in REAL implies (((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) . x = (cos . x) ^2 )
assume x in REAL ; :: thesis: (((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) . x = (cos . x) ^2
(((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) . x = (diff (AffineMap (1 / 2),0 ),x) + (diff ((1 / 4) (#) (sin * (AffineMap 2,0 ))),x) by A4, A6, A3, FDIFF_1:26
.= (((AffineMap (1 / 2),0 ) `| REAL ) . x) + (diff ((1 / 4) (#) (sin * (AffineMap 2,0 ))),x) by A6, FDIFF_1:def 8
.= (1 / 2) + (diff ((1 / 4) (#) (sin * (AffineMap 2,0 ))),x) by A5, Lm1, FDIFF_1:31
.= (1 / 2) + ((((1 / 4) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x) by A3, FDIFF_1:def 8
.= (1 / 2) + ((1 / 2) * (cos (2 * x))) by A7
.= (1 + (cos (2 * x))) / 2
.= (cos x) ^2 by SIN_COS5:21 ;
hence (((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) `| REAL ) . x = (cos . x) ^2 ; :: thesis: verum

end;

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