let n be non zero Nat; :: thesis: (@ ((@ sin) |^ (n + 1))) `| REAL = ((n + 1) (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos))
set Z = REAL ;
set x = sin ;
defpred S<sub>1</sub>[ Nat] means (@ ((@ sin) |^ ($1 + 1))) `| REAL = (($1 + 1) (#) (@ ((@ sin) |^ $1))) (#) (@ (@ cos));
A1: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
reconsider n1 = n + 1 as non zero Nat ;
A3: ( @ ((@ sin) |^ n1) is_differentiable_on REAL & @ (@ sin) is_differentiable_on REAL ) by Lm7, SIN_COS:68, Th24;
A4: @ ((@ sin) |^ n1) = ((@ sin) |^ n) * (@ sin) by Th20
.= (@ ((@ sin) |^ n)) (#) (@ (@ sin)) by Th13 ;
reconsider f = (@ ((@ sin) |^ n1)) (#) (@ (@ cos)) as Function of REAL,REAL ;
reconsider f1 = f as Element of (RAlgebra REAL) by FUNCT_2:8;
reconsider r1 = n1 as Element of REAL by NUMBERS:19;
reconsider o1 = 1 as Element of REAL by FINANCE2:1;
A5: f = @ f1 ;
A6: r1 (#) (@ f1) = @ (r1 * f1) by Th14;
A7: 1 (#) (@ f1) = @ (o1 * f1) by Th14;
((n1 (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos))) (#) (@ (@ sin)) = ((n1 (#) (@ ((@ sin) |^ n))) (#) (@ (@ sin))) (#) (@ (@ cos)) by RFUNCT_1:9
.= (n1 (#) (@ ((@ sin) |^ n1))) (#) (@ (@ cos)) by A4, RFUNCT_1:12 ;
then A9: (((n1 (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos))) (#) (@ (@ sin))) + ((@ ((@ sin) |^ n1)) (#) cos) = (@ (r1 * f1)) + (@ (o1 * f1)) by A7, A6, RFUNCT_1:12
.= (r1 * f1) + (o1 * f1) by Th18
.= (r1 + o1) * f1 by FUNCSDOM:14
.= (n1 + 1) (#) ((@ ((@ sin) |^ n1)) (#) (@ (@ cos))) by A5, Th14 ;
@ ((@ sin) |^ (n1 + 1)) = ((@ sin) |^ n1) * (@ sin) by Th20
.= (@ ((@ sin) |^ n1)) (#) (@ (@ sin)) by Th13 ;
then (@ ((@ sin) |^ (n1 + 1))) `| REAL = (n1 + 1) (#) ((@ ((@ sin) |^ n1)) (#) (@ (@ cos))) by A9, A2, A3, Lm7, FDIFF_2:20, INTEGRA8:27
.= ((n1 + 1) (#) (@ ((@ sin) |^ n1))) (#) (@ (@ cos)) by RFUNCT_1:12 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A11: S₁[1]

proof

A12: @ ((@ sin) |^ 1) = @ (@ sin) by BINOM:8;
@ ((@ sin) |^ (1 + 1)) = ((@ sin) |^ 1) * (@ sin) by Th20
.= (@ ((@ sin) |^ 1)) (#) (@ (@ sin)) by Th13 ;
then (@ ((@ sin) |^ (1 + 1))) `| REAL = ((@ (@ sin)) (#) cos) + ((@ (@ sin)) (#) cos) by A12, SIN_COS:68, Lm7, FDIFF_2:20, INTEGRA8:27
.= 2 (#) ((@ ((@ sin) |^ 1)) (#) (@ (@ cos))) by A12, PDLAX:9 ;
hence S₁[1] by RFUNCT_1:12; :: thesis: verum

end;

for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A11, A1);
hence (@ ((@ sin) |^ (n + 1))) `| REAL = ((n + 1) (#) (@ ((@ sin) |^ n))) (#) (@ (@ cos)) ; :: thesis: verum