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