scheme :: YELLOW17:sch 1
ElProductEx{ F₁() -> non empty set , F₂() -> non-Empty TopStruct-yielding ManySortedSet of F₁(), P₁[ object , object ] } :

ex f being Element of (product F₂()) st
for i being Element of F₁() holds P₁[f . i,i]

provided

A1: for i being Element of F₁() ex x being Element of (F₂() . i) st P₁[x,i]