theorem Th22: :: PARTFUN1:22

for X, Y being set
for f being Function holds <:f,X,Y:> c= f