set x = sin ;
let n be Nat; :: thesis: ( n >= 2 implies @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL )
assume A1: n >= 2 ; :: thesis: @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL
then A2: n -' 2 = n - 2 by XREAL_1:233;
reconsider n2 = n -' 2 as Nat ;
A3: n -' 1 = n - 1 by A1, XXREAL_0:2, XREAL_1:233;
reconsider n1 = n -' 1 as Nat ;
reconsider f = ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)) as Function of REAL,REAL ;
reconsider F = @ ((@ sin) |^ (n -' 1)) as Function of REAL,REAL ;

per cases ( n = 2 or n > 2 ) by A1, XXREAL_0:1;

suppose A4: n = 2 ; :: thesis: @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL

then A5: @ ((@ sin) |^ (n -' 1)) = sin by A3, BINOM:8;
A6: (@ sin) |^ (n -' 2) = (@ sin) |^ 0 by A4, XREAL_1:232
.= 1_ (RAlgebra REAL) by BINOM:8 ;
((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)) = ((@ sin) |^ (n -' 2)) * (@ cos) by Th13, A3, A4
.= cos by A6 ;
then A8: (((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos))) | REAL = (@ ((@ sin) |^ (n -' 1))) `| REAL by A5, INTEGRA8:27;
@ ((@ sin) |^ (n -' 1)) in IntegralFuncs (f,REAL) by A8, A5, SIN_COS:68, INTEGRA7:def 1;
hence @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL by INTEGRA7:def 2; :: thesis: verum

end;

suppose A10: n > 2 ; :: thesis: @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL

then reconsider n2 = n2 as non zero Nat by A2;
A11: n2 + 1 = (n - 2) + 1 by A1, XREAL_1:233
.= n - 1
.= n -' 1 by A1, XXREAL_0:2, XREAL_1:233 ;
A12: n - 1 > 2 - 1 by A10, XREAL_1:14;
reconsider n1 = n1 as non zero Nat by A12, A1, XXREAL_0:2, XREAL_1:233;
A13: @ ((@ sin) |^ n1) is_differentiable_on REAL by Lm7, SIN_COS:68, Th24;
f | REAL = F `| REAL by Th28, A11;
then @ ((@ sin) |^ (n -' 1)) in IntegralFuncs (f,REAL) by A13, INTEGRA7:def 1;
hence @ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL by INTEGRA7:def 2; :: thesis: verum

end;

end;