for p being Prime
for F being Z/ b₁ -homomorphic b₁ -characteristic Field
for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)