:: deftheorem Def4 defines pr1 FUNCT_3:def 4 :
for X, Y being set
for b₃ being Function holds
( b₃ = pr1 (X,Y) iff ( dom b₃ = [:X,Y:] & ( for x, y being object st x in X & y in Y holds
b₃ . (x,y) = x ) ) );