:: deftheorem defines <: PARTFUN1:def 1 :
for f being Function
for X, Y being set holds <:f,X,Y:> = (Y |` f) | X;