scheme :: YELLOW18:sch 23
NonUniqMSFunctionEx{ F1() -> set , F2() -> ManySortedSet of F1(), F3() -> ManySortedSet of F1(), P1[ object , object , object ] } :
ex F being ManySortedFunction of F2(),F3() st
for i, x being object st i in F1() & x in F2() . i holds
( (F . i) . x in F3() . i & P1[i,x,(F . i) . x] )
provided
A1: for i, x being object st i in F1() & x in F2() . i holds
ex y being object st
( y in F3() . i & P1[i,x,y] )