let n be Element of NAT ; :: thesis: ( (1 / (n + 1)) (#) ((#Z (n + 1)) * sin) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) ) )
A1: [#] REAL = dom ((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) by FUNCT_2:def 1;
for x0 being Real holds (#Z (n + 1)) * sin is_differentiable_in x0

proof

let x0 be Real; :: thesis: (#Z (n + 1)) * sin is_differentiable_in x0
sin is_differentiable_in x0 by SIN_COS:64;
hence (#Z (n + 1)) * sin is_differentiable_in x0 by TAYLOR_1:3; :: thesis: verum

end;

then ( [#] REAL = dom ((#Z (n + 1)) * sin) & ( for x0 being Real st x0 in REAL holds
(#Z (n + 1)) * sin is_differentiable_in x0 ) ) by FUNCT_2:def 1;
then A2: (#Z (n + 1)) * sin is_differentiable_on REAL by FDIFF_1:9;
hence (1 / (n + 1)) (#) ((#Z (n + 1)) * sin) is_differentiable_on REAL by A1, FDIFF_1:20; :: thesis: for x being Real holds (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x)
A3: for x being Real st x in REAL holds
(((#Z (n + 1)) * sin) `| REAL) . x = ((n + 1) * ((sin . x) #Z n)) * (cos . x)

proof

set m = n + 1;
let x be Real; :: thesis: ( x in REAL implies (((#Z (n + 1)) * sin) `| REAL) . x = ((n + 1) * ((sin . x) #Z n)) * (cos . x) )
assume A4: x in REAL ; :: thesis: (((#Z (n + 1)) * sin) `| REAL) . x = ((n + 1) * ((sin . x) #Z n)) * (cos . x)
sin is_differentiable_in x by SIN_COS:64;
then diff (((#Z (n + 1)) * sin),x) = ((n + 1) * ((sin . x) #Z ((n + 1) - 1))) * (diff (sin,x)) by TAYLOR_1:3
.= ((n + 1) * ((sin . x) #Z ((n + 1) - 1))) * (cos . x) by SIN_COS:64 ;
hence (((#Z (n + 1)) * sin) `| REAL) . x = ((n + 1) * ((sin . x) #Z n)) * (cos . x) by A2, FDIFF_1:def 7, A4; :: thesis: verum

end;

A5: for x being Real st x in REAL holds
(((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x)

proof

let x be Real; :: thesis: ( x in REAL implies (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) )
assume A6: x in REAL ; :: thesis: (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x)
(((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = (1 / (n + 1)) * (diff (((#Z (n + 1)) * sin),x)) by A1, A2, FDIFF_1:20, A6
.= (1 / (n + 1)) * ((((#Z (n + 1)) * sin) `| REAL) . x) by A2, FDIFF_1:def 7, A6
.= (1 / (n + 1)) * (((n + 1) * ((sin . x) #Z n)) * (cos . x)) by A3, A6
.= (((1 / (n + 1)) * (n + 1)) * ((sin . x) #Z n)) * (cos . x)
.= (((n + 1) / (n + 1)) * ((sin . x) #Z n)) * (cos . x) by XCMPLX_1:99
.= (1 * ((sin . x) #Z n)) * (cos . x) by XCMPLX_1:60 ;
hence (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) ; :: thesis: verum

end;

let x be Real; :: thesis: (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x)
x in REAL by XREAL_0:def 1;
hence (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) by A5; :: thesis: verum