Frob F = (Frob F) `^ 1 ;
hence Frob F is RingIsomorphism ; :: thesis: verum