:: deftheorem canH defines canHom MOEBIUS2:def 7 :
for p being Prime
for b₂ being Function of (FreeGen p),(BoolePrime p) holds
( b₂ = canHom p iff for x being Element of FreeGen p holds b₂ . x = (pfexp x) | ((Seg p) /\ SetPrimes) );