scheme :: MSAFREE5:sch 5
LambdaTerm{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty ManySortedSet of the carrier of F₁(), F₃() -> F₂(),F₁() -terms all_vars_including inheriting_operations MSAlgebra over F₁(), F₄() -> F₂(),F₁() -terms all_vars_including inheriting_operations MSAlgebra over F₁(), F₅( object ) -> Element of F₄() } :

ex f being ManySortedFunction of F₃(),F₄() st
for t being Element of F₃() holds f . t = F₅(t)

provided

A0: for t being Element of F₃() holds the_sort_of t = the_sort_of F₅(t)