let n be non zero Nat; :: thesis: (@ ((@ sin) |^ (n + 1))) `| REAL is_differentiable_on REAL
set Z = REAL ;
set x = sin ;
A1: ( @ ((@ sin) |^ n) is_differentiable_on REAL & @ (@ sin) is_differentiable_on REAL ) by Lm7, SIN_COS:68, Th24;
((n + 1) (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos)) is_differentiable_on REAL

proof

reconsider h = (@ ((@ sin) |^ n)) (#) (@ (@ cos)) as Function of REAL,REAL ;
h is_differentiable_on REAL by A1, SIN_COS:67, INTEGRA7:6;
then (n + 1) (#) ((@ ((@ sin) |^ n)) (#) (@ (@ cos))) is_differentiable_on REAL by INTEGRA7:7;
hence ((n + 1) (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos)) is_differentiable_on REAL by RFUNCT_1:12; :: thesis: verum

end;

hence (@ ((@ sin) |^ (n + 1))) `| REAL is_differentiable_on REAL by Th28; :: thesis: verum