let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for f being Element of the carrier of (Polynom-Ring R) holds
( (Deriv R) . f = 0_. R iff for i being Nat st i in Support f holds
p divides i )
let R be commutative p -characteristic Ring; :: thesis: for f being Element of the carrier of (Polynom-Ring R) holds
( (Deriv R) . f = 0_. R iff for i being Nat st i in Support f holds
p divides i )
let f be Element of the carrier of (Polynom-Ring R); :: thesis: ( (Deriv R) . f = 0_. R iff for i being Nat st i in Support f holds
p divides i )
set q = (Deriv R) . f;

A: now :: thesis: ( ( for i being Nat st i in Support f holds
p divides i ) implies (Deriv R) . f = 0_. R )

assume AS: for i being Nat st i in Support f holds
p divides i ; :: thesis: (Deriv R) . f = 0_. R

now :: thesis: for j being Nat holds ((Deriv R) . f) . j = (0_. R) . j

let j be Nat; :: thesis: ((Deriv R) . f) . b₁ = (0_. R) . b₁
B: ((Deriv R) . f) . j = (j + 1) * (f . (j + 1)) by RINGDER1:def 8;

per cases ( j + 1 in Support f or not j + 1 in Support f ) ;

suppose j + 1 in Support f ; :: thesis: ((Deriv R) . f) . b₁ = (0_. R) . b₁

hence ((Deriv R) . f) . j = 0. R by B, AS, Lm2
.= (0_. R) . j by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose not j + 1 in Support f ; :: thesis: ((Deriv R) . f) . b₁ = (0_. R) . b₁

hence ((Deriv R) . f) . j = (j + 1) * (0. R) by B, POLYNOM1:def 4
.= (0_. R) . j by ORDINAL1:def 12, FUNCOP_1:7 ;
:: thesis: verum

end;

end;

end;

hence (Deriv R) . f = 0_. R ; :: thesis: verum

end;

now :: thesis: ( (Deriv R) . f = 0_. R implies for i being Nat st i in Support f holds
p divides i )

assume AS: (Deriv R) . f = 0_. R ; :: thesis: for i being Nat st i in Support f holds
p divides i

now :: thesis: for j being Nat holds
( not j in Support f or p divides j )

assume ex j being Nat st
( j in Support f & not p divides j ) ; :: thesis: contradiction
then consider j being Nat such that
B: ( j in Support f & not p divides j ) ;
C: not f . j is zero by B, POLYNOM1:def 3;
p * 0 = 0 ;
then j <> 0 by B, NAT_D:def 3;
then reconsider j1 = j - 1 as Nat ;
j1 + 1 = j ;
then ((Deriv R) . f) . j1 = j * (f . j) by RINGDER1:def 8;
then ((Deriv R) . f) . j1 <> 0. R by B, C, Lm2a;
hence contradiction by AS, ORDINAL1:def 12, FUNCOP_1:7; :: thesis: verum

end;

hence for i being Nat st i in Support f holds
p divides i ; :: thesis: verum

end;

hence ( (Deriv R) . f = 0_. R iff for i being Nat st i in Support f holds
p divides i ) by A; :: thesis: verum