set f = Frob R;
H: Char R = p by RING_3:def 6;

now :: thesis: for x1, x2 being object st x1 in the carrier of R & x2 in the carrier of R & (Frob R) . x1 = (Frob R) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of R & x2 in the carrier of R & (Frob R) . x1 = (Frob R) . x2 implies x1 = x2 )
assume A: ( x1 in the carrier of R & x2 in the carrier of R & (Frob R) . x1 = (Frob R) . x2 ) ; :: thesis: x1 = x2
then reconsider a = x1, b = x2 as Element of R ;
0. R = ((Frob R) . a) - ((Frob R) . b) by A, RLVECT_1:15
.= (a |^ p) - ((Frob R) . b) by H, defFr
.= (a |^ p) - (b |^ p) by H, defFr
.= (a |^ p) + ((- b) |^ p) by FIELD_15:42
.= (a + (- b)) |^ p by FIELD_15:40 ;
then a - b is nilpotent by TOPZARI1:def 2;
then a - b = 0. R by NIL1;
hence x1 = x2 by RLVECT_1:21; :: thesis: verum

end;

hence Frob R is one-to-one by FUNCT_2:19; :: thesis: verum