theorem Th29: :: PARTFUN1:29

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