scheme :: PRE_CIRC:sch 2
MSSLambda2Part{ F₁() -> set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being ManySortedSet of F₁() st
for i being Element of F₁() st i in F₁() holds
( ( P₁[i] implies f . i = F₂(i) ) & ( P₁[i] implies f . i = F₃(i) ) )