let R be non degenerated commutative Ring; :: thesis: for n being non trivial Nat
for a being Element of R holds (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R)))
let n be non trivial Nat; :: thesis: for a being Element of R holds (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R)))
let a be Element of R; :: thesis: (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R)))
set q = X^ (n,a);
set D = (Deriv R) . (X^ (n,a));
reconsider p = n * (X^ ((n - 1),(0. R))) as Polynomial of R by POLYNOM3:def 10;
A: ( n <> 0 & n <> 1 ) by NAT_2:def 1;

now :: thesis: for o being object st o in NAT holds
((Deriv R) . (X^ (n,a))) . o = p . o

let o be object ; :: thesis: ( o in NAT implies ((Deriv R) . (X^ (n,a))) . b₁ = p . b₁ )
assume o in NAT ; :: thesis: ((Deriv R) . (X^ (n,a))) . b₁ = p . b₁
then reconsider j = o as Element of NAT ;

per cases ( j = 0 or j = n - 1 or ( j <> 0 & j <> n - 1 ) ) ;

suppose C: j = 0 ; :: thesis: ((Deriv R) . (X^ (n,a))) . b₁ = p . b₁

hence ((Deriv R) . (X^ (n,a))) . o = (0 + 1) * ((X^ (n,a)) . (0 + 1)) by RINGDER1:def 8
.= 1 * (0. R) by A, Lm11
.= n * (0. R)
.= n * ((X^ ((n - 1),(0. R))) . j) by C, Lm10
.= p . o by BBB ;
:: thesis: verum

end;

suppose C: j = n - 1 ; :: thesis: ((Deriv R) . (X^ (n,a))) . b₁ = p . b₁

hence ((Deriv R) . (X^ (n,a))) . o = ((n - 1) + 1) * ((X^ (n,a)) . ((n - 1) + 1)) by RINGDER1:def 8
.= n * (1. R) by Lm10
.= n * ((X^ ((n - 1),(0. R))) . j) by C, Lm10
.= p . o by BBB ;
:: thesis: verum

end;

suppose C: ( j <> 0 & j <> n - 1 ) ; :: thesis: ((Deriv R) . (X^ (n,a))) . b₁ = p . b₁

then D: j + 1 <> n ;
thus ((Deriv R) . (X^ (n,a))) . o = (j + 1) * ((X^ (n,a)) . (j + 1)) by RINGDER1:def 8
.= (j + 1) * (0. R) by D, Lm11
.= n * (0. R)
.= n * ((X^ ((n - 1),(0. R))) . j) by C, Lm11
.= p . o by BBB ; :: thesis: verum

end;

end;

end;

hence (Deriv R) . (X^ (n,a)) = n * (X^ ((n - 1),(0. R))) by FUNCT_2:12; :: thesis: verum