scheme :: INSTALG1:sch 1
GenFuncEx{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> V2() ManySortedSet of the carrier of F₁(), F₄( object , object ) -> set } :

ex h being ManySortedFunction of (FreeMSA F₃()),F₂() st
( h is_homomorphism FreeMSA F₃(),F₂() & ( for s being SortSymbol of F₁()
for x being Element of F₃() . s holds (h . s) . (root-tree [x,s]) = F₄(x,s) ) )

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₃() . s holds F₄(x,s) in the Sorts of F₂() . s