theorem Th28: :: PARTFUN1:28

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