:: deftheorem Def1 defines -hash BIRKHOFF:def 1 :
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of X, the Sorts of A
for b₅ being ManySortedFunction of (FreeMSA X),A holds
( b₅ = F -hash iff ( b₅ is_homomorphism FreeMSA X,A & b₅ || (FreeGen X) = F ** (Reverse X) ) );