A1: for x being Real st x in REAL holds
(AffineMap (2,0)) . x = (2 * x) + 0 by FCONT_1:def 4;
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:20;
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 FCONT_1:def 4;
then A6: AffineMap ((1 / 2),0) is_differentiable_on REAL by Lm1, FDIFF_1:23;
hence (AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0)))) is_differentiable_on REAL by A4, A3, FDIFF_1:18; :: thesis: for x being Real holds (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2
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 A8: 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:20, A8
.= (1 / 4) * (((sin * (AffineMap (2,0))) `| REAL) . x) by A2, FDIFF_1:def 7, A8
.= (1 / 4) * (2 * (cos . ((2 * x) + 0))) by A1, Lm2, FDIFF_4:37, A8
.= (1 / 2) * (cos (2 * x)) ;
hence (((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . x = (1 / 2) * (cos (2 * x)) ; :: thesis: verum

end;

A9: 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 A10: 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:18, A10
.= (((AffineMap ((1 / 2),0)) `| REAL) . x) + (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),x)) by A6, FDIFF_1:def 7, A10
.= (1 / 2) + (diff (((1 / 4) (#) (sin * (AffineMap (2,0)))),x)) by A5, Lm1, FDIFF_1:23, A10
.= (1 / 2) + ((((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . x) by A3, FDIFF_1:def 7, A10
.= (1 / 2) + ((1 / 2) * (cos (2 * x))) by A7, A10
.= (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;

let x be Real; :: thesis: (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2
x in REAL by XREAL_0:def 1;
hence (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2 by A9; :: thesis: verum