scheme :: FILTER_1:sch 5
AuxCart2{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ] } :

for d, d9 being Element of [:F₁(),F₂():] holds P₁[d,d9]

provided

A1: for d1, d19 being Element of F₁()
for d2, d29 being Element of F₂() holds P₁[[d1,d2],[d19,d29]]