scheme :: YELLOW17:sch 1
ElProductEx{ F1() -> non empty set , F2() -> non-Empty TopStruct-yielding ManySortedSet of F1(), P1[ object , object ] } :
ex f being Element of (product F2()) st
for i being Element of F1() holds P1[f . i,i]
provided
A1: for i being Element of F1() ex x being Element of (F2() . i) st P1[x,i]