let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being Element of R
for n being Nat holds (n * p) * a = 0. R
let R be commutative p -characteristic Ring; :: thesis: for a being Element of R
for n being Nat holds (n * p) * a = 0. R
let a be Element of R; :: thesis: for n being Nat holds (n * p) * a = 0. R
let n be Nat; :: thesis: (n * p) * a = 0. R
defpred S₁[ Nat] means ($1 * p) * a = 0. R;
IA: S₁[ 0 ] by BINOM:12;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]
((k + 1) * p) * a = ((k * p) + p) * a
.= ((k * p) * a) + (p * a) by BINOM:15
.= 0. R by IV, Lm0 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence (n * p) * a = 0. R ; :: thesis: verum