A3: dom ((AffineMap (1 / 2),0 ) + ((1 / 4) (#) (sin * (AffineMap 2,0 )))) = [#] REAL by FUNCT_2:def 1;
B: for x being Real st x in REAL holds
(AffineMap (1 / 2),0 ) . x = ((1 / 2) * x) + 0 by JORDAN16:def 3;
then A4: ( AffineMap (1 / 2),0 is_differentiable_on REAL & ( for x being Real st x in REAL holds
((AffineMap (1 / 2),0 ) `| REAL ) . x = 1 / 2 ) ) by A1, FDIFF_1:31;
A5: for x being Real st x in REAL holds
(AffineMap 2,0 ) . x = (2 * x) + 0 by JORDAN16:def 3;
then A6: ( 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;
then A7: (1 / 4) (#) (sin * (AffineMap 2,0 )) is_differentiable_on REAL by A2, FDIFF_1:28;
A8: 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, A6, FDIFF_1:28
.= (1 / 4) * (((sin * (AffineMap 2,0 )) `| REAL ) . x) by A6, FDIFF_1:def 8
.= (1 / 4) * (2 * (cos . ((2 * x) + 0 ))) by A1, A5, 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 A3, A4, A7, FDIFF_1:26
.= (((AffineMap (1 / 2),0 ) `| REAL ) . x) + (diff ((1 / 4) (#) (sin * (AffineMap 2,0 ))),x) by A4, FDIFF_1:def 8
.= (1 / 2) + (diff ((1 / 4) (#) (sin * (AffineMap 2,0 ))),x) by B, A1, FDIFF_1:31
.= (1 / 2) + ((((1 / 4) (#) (sin * (AffineMap 2,0 ))) `| REAL ) . x) by A7, FDIFF_1:def 8
.= (1 / 2) + ((1 / 2) * (cos (2 * x))) by A8
.= (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 A3, A4, A7, FDIFF_1:26; :: thesis: verum