set F = R;
set Fp = R |^ p;
A: the carrier of (R |^ p) = { (a |^ p) where a is Element of R : verum } by deffp;

now :: thesis: for o being object st o in the carrier of (R |^ p) holds
o in the carrier of R

let o be object ; :: thesis: ( o in the carrier of (R |^ p) implies o in the carrier of R )
assume o in the carrier of (R |^ p) ; :: thesis: o in the carrier of R
then consider b being Element of R such that
H: o = b |^ p by A;
thus o in the carrier of R by H; :: thesis: verum

end;

then B: the carrier of (R |^ p) c= the carrier of R ;
( the addF of (R |^ p) = the addF of R || the carrier of (R |^ p) & the multF of (R |^ p) = the multF of R || the carrier of (R |^ p) & 1. (R |^ p) = 1. R & 0. (R |^ p) = 0. R ) by deffp;
then R |^ p is Subring of R by B, C0SP1:def 3;
hence R |^ p is p -characteristic ; :: thesis: verum