scheme :: PRE_CIRC:sch 4
LambdaMSFD{ F₁() -> non empty set , F₂() -> Subset of F₁(), F₃() -> ManySortedSet of F₂(), F₄() -> ManySortedSet of F₂(), F₅( object ) -> set } :

ex f being ManySortedFunction of F₃(),F₄() st
for i being Element of F₁() st i in F₂() holds
f . i = F₅(i)

provided

A1: for i being Element of F₁() st i in F₂() holds
F₅(i) is Function of (F₃() . i),(F₄() . i)