let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for a being Element of R holds p * a = 0. R
let R be commutative p -characteristic Ring; :: thesis: for a being Element of R holds p * a = 0. R
let a be Element of R; :: thesis: p * a = 0. R
B: Char R = p by RING_3:def 6;
consider n being Nat such that
A: ( ( p = n & p '*' a = n * a ) or ( p = - n & p '*' a = - (n * a) ) ) by RING_3:def 2;
thus p * a = p '*' (a * (1. R)) by A
.= (p '*' (1. R)) * a by REALALG2:5
.= (0. R) * a by B, RING_3:def 5
.= 0. R ; :: thesis: verum