theorem :: FUNCT_1:57

for X, Y being set
for f being Function st X c= Y holds
( Y |` (X |` f) = X |` f & X |` (Y |` f) = X |` f ) by RELAT_1:98, RELAT_1:99;