scheme :: MSAFREE5:sch 5
LambdaTerm{ F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of the carrier of F1(), F3() -> F2(),F1() -terms all_vars_including inheriting_operations MSAlgebra over F1(), F4() -> F2(),F1() -terms all_vars_including inheriting_operations MSAlgebra over F1(), F5( object ) -> Element of F4() } :
ex f being ManySortedFunction of F3(),F4() st
for t being Element of F3() holds f . t = F5(t)
provided
A0: for t being Element of F3() holds the_sort_of t = the_sort_of F5(t)