ex f being Function st
for x, y being object holds
( [x,y] in f iff ( x in F₁() & P₁[x,y] ) )

A1: for x, y1, y2 being object st P₁[x,y1] & P₁[x,y2] holds
y1 = y2