scheme :: NAT_1:sch 19
SeqEx2D{ F1() -> non empty set , F2() -> non empty set , P1[ set , set , set ] } :
ex f being Function of [:F1(),NAT:],F2() st
for x being Element of F1()
for y being Nat holds P1[x,y,f . (x,y)]
provided
A1: for x being Element of F1()
for y being Nat ex z being Element of F2() st P1[x,y,z]