scheme :: YELLOW18:sch 23
NonUniqMSFunctionEx{ F₁() -> set , F₂() -> ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ object , object , object ] } :

ex F being ManySortedFunction of F₂(),F₃() st
for i, x being object st i in F₁() & x in F₂() . i holds
( (F . i) . x in F₃() . i & P₁[i,x,(F . i) . x] )

provided

A1: for i, x being object st i in F₁() & x in F₂() . i holds
ex y being object st
( y in F₃() . i & P₁[i,x,y] )