:: deftheorem defines |= EQUATION:def 5 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds
( A |= e iff for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e `1) = (h . s) . (e `2) );