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; 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;
( x in REAL implies (((1 / 4) (#) (sin * (AffineMap (2,0)))) `| REAL) . x = (1 / 2) * (cos (2 * x)) )
assume A8:
x in REAL
;
(((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))
;
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;
( x in REAL implies (((AffineMap ((1 / 2),0)) + ((1 / 4) (#) (sin * (AffineMap (2,0))))) `| REAL) . x = (cos . x) ^2 )
assume A10:
x in REAL
;
(((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
;
verum
end;
let x be Real; (((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; verum