let R be non degenerated commutative Ring; :: thesis: ker (Frob R) c= nilrad R
H1: nilrad R = { a where a is nilpotent Element of R : verum } by TOPZARI1:def 13;
set n = Char R;
R is Char R -characteristic by RING_3:def 6;
then H2: ker (Frob R) = { a where a is Element of R : a |^ (Char R) = 0. R } by FrK;

now :: thesis: for o being object st o in ker (Frob R) holds
o in nilrad R

let o be object ; :: thesis: ( o in ker (Frob R) implies o in nilrad R )
assume o in ker (Frob R) ; :: thesis: o in nilrad R
then consider a being Element of R such that
A: ( o = a & a |^ (Char R) = 0. R ) by H2;

now :: thesis: not Char R = 0

assume Char R = 0 ; :: thesis: contradiction
then a |^ (Char R) = 1_ R by BINOM:8;
hence contradiction by A; :: thesis: verum

end;

then a is nilpotent by A, TOPZARI1:def 2;
hence o in nilrad R by A, H1; :: thesis: verum

end;

hence ker (Frob R) c= nilrad R ; :: thesis: verum