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