let p be Nat; :: thesis: for R being p -characteristic Ring holds ker (Frob R) = { a where a is Element of R : a |^ p = 0. R }
let R be p -characteristic Ring; :: thesis: ker (Frob R) = { a where a is Element of R : a |^ p = 0. R }
set f = Frob R;
H: ker (Frob R) = { v where v is Element of R : (Frob R) . v = 0. R } by VECTSP10:def 9;
I: Char R = p by RING_3:def 6;

A: now :: thesis: for o being object st o in ker (Frob R) holds
o in { a where a is Element of R : a |^ p = 0. R }

let o be object ; :: thesis: ( o in ker (Frob R) implies o in { a where a is Element of R : a |^ p = 0. R } )
assume o in ker (Frob R) ; :: thesis: o in { a where a is Element of R : a |^ p = 0. R }
then consider a being Element of R such that
B: ( o = a & (Frob R) . a = 0. R ) by H;
(Frob R) . a = a |^ p by I, defFr;
hence o in { a where a is Element of R : a |^ p = 0. R } by B; :: thesis: verum

end;

now :: thesis: for o being object st o in { a where a is Element of R : a |^ p = 0. R } holds
o in ker (Frob R)

let o be object ; :: thesis: ( o in { a where a is Element of R : a |^ p = 0. R } implies o in ker (Frob R) )
assume o in { a where a is Element of R : a |^ p = 0. R } ; :: thesis: o in ker (Frob R)
then consider a being Element of R such that
B: ( o = a & a |^ p = 0. R ) ;
(Frob R) . a = 0. R by I, B, defFr;
hence o in ker (Frob R) by B, H; :: thesis: verum

end;

hence ker (Frob R) = { a where a is Element of R : a |^ p = 0. R } by A, TARSKI:2; :: thesis: verum