set p = Char F;
reconsider F = F as Char F -characteristic Field by RING_3:def 6;
reconsider A = the carrier of F as finite set ;
reconsider B = the carrier of F as finite set ;
reconsider f = Frob F as Function of A,B ;
( card A = card B & f is one-to-one ) ;
hence Frob F is onto by FINSEQ_4:63; :: thesis: verum