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

now :: thesis: for x, y being Element of R holds (Frob R) . (x + y) = ((Frob R) . x) + ((Frob R) . y)

let x, y be Element of R; :: thesis: (Frob R) . (x + y) = ((Frob R) . x) + ((Frob R) . y)
thus (Frob R) . (x + y) = (x + y) |^ p by H, defFr
.= (x |^ p) + (y |^ p) by FIELD_15:40
.= (x |^ p) + ((Frob R) . y) by H, defFr
.= ((Frob R) . x) + ((Frob R) . y) by H, defFr ; :: thesis: verum

end;

hence Frob R is additive ; :: thesis: ( Frob R is multiplicative & Frob R is unity-preserving )

now :: thesis: for x, y being Element of R holds (Frob R) . (x * y) = ((Frob R) . x) * ((Frob R) . y)

let x, y be Element of R; :: thesis: (Frob R) . (x * y) = ((Frob R) . x) * ((Frob R) . y)
thus (Frob R) . (x * y) = (x * y) |^ p by H, defFr
.= (x |^ p) * (y |^ p) by BINOM:9
.= (x |^ p) * ((Frob R) . y) by H, defFr
.= ((Frob R) . x) * ((Frob R) . y) by H, defFr ; :: thesis: verum

end;

hence Frob R is multiplicative ; :: thesis: Frob R is unity-preserving
thus (Frob R) . (1_ R) = (1_ R) |^ p by H, defFr
.= 1_ R ; :: according to GROUP_1:def 13 :: thesis: verum