scheme :: BIRKHOFF:sch 4
EqTerms{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of F₂(), F₄() -> SortSymbol of F₁(), F₅() -> Element of the Sorts of (TermAlg F₁()) . F₄(), F₆() -> Element of the Sorts of (TermAlg F₁()) . F₄(), P₁[ set ] } :

for B being non-empty MSAlgebra over F₁() st P₁[B] holds
B |= F₅() '=' F₆()

provided

A1: ((F₃() -hash) . F₄()) . F₅() = ((F₃() -hash) . F₄()) . F₆() and
A2: for C being non-empty MSAlgebra over F₁()
for G being ManySortedFunction of the carrier of F₁() --> NAT, the Sorts of C st P₁[C] holds
ex h being ManySortedFunction of F₂(),C st
( h is_homomorphism F₂(),C & G = h ** F₃() )