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