theorem :: PARTFUN1:30

for X1, X2, Y1, Y2 being set
for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>