let p be prime Nat; :: thesis: Frob (Z/ p) = id (Z/ p)
I: Char (Z/ p) = p by RING_3:77;

now :: thesis: for o being object st o in the carrier of (Z/ p) holds
(Frob (Z/ p)) . o = (id (Z/ p)) . o

let o be object ; :: thesis: ( o in the carrier of (Z/ p) implies (Frob (Z/ p)) . o = (id (Z/ p)) . o )
assume o in the carrier of (Z/ p) ; :: thesis: (Frob (Z/ p)) . o = (id (Z/ p)) . o
then reconsider a = o as Element of (Z/ p) ;
thus (Frob (Z/ p)) . o = a |^ p by I, defFr
.= (id (Z/ p)) . o by fresh3 ; :: thesis: verum

end;

hence Frob (Z/ p) = id (Z/ p) ; :: thesis: verum