let p be Prime; :: thesis: for R being commutative p -characteristic Ring
for x being Element of (R |^ p) holds x is Element of R
let F be commutative p -characteristic Ring; :: thesis: for x being Element of (F |^ p) holds x is Element of F
let x be Element of (F |^ p); :: thesis: x is Element of F
A: the carrier of (F |^ p) = { (a |^ p) where a is Element of F : verum } by deffp;
x in the carrier of (F |^ p) ;
then consider a being Element of F such that
B: x = a |^ p by A;
thus x is Element of F by B; :: thesis: verum