scheme :: FUNCT_3:sch 1
FuncEx3{ F₁() -> set , F₂() -> set , P₁[ object , object , object ] } :

ex f being Function st
( dom f = [:F₁(),F₂():] & ( for x, y being object st x in F₁() & y in F₂() holds
P₁[x,y,f . (x,y)] ) )

provided

A1: for x, y, z1, z2 being object st x in F₁() & y in F₂() & P₁[x,y,z1] & P₁[x,y,z2] holds
z1 = z2 and
A2: for x, y being object st x in F₁() & y in F₂() holds
ex z being object st P₁[x,y,z]