let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being Element of R
for n being Nat st p divides n holds
n * a = 0. R
let R be commutative p -characteristic Ring; :: thesis: for a being Element of R
for n being Nat st p divides n holds
n * a = 0. R
let a be Element of R; :: thesis: for n being Nat st p divides n holds
n * a = 0. R
let n be Nat; :: thesis: ( p divides n implies n * a = 0. R )
assume p divides n ; :: thesis: n * a = 0. R
then ex x being Nat st p * x = n by NAT_D:def 3;
hence n * a = 0. R by Lm1; :: thesis: verum