theorem :: PARTFUN1:33

for X, Y being set
for f being PartFunc of X,Y holds <:f,X,Y:> = f ;