theorem :: PARTFUN1:27

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