theorem Th31: :: PARTFUN1:31

for X, Y being set
for f being Function st dom f c= X & rng f c= Y holds
f = <:f,X,Y:>