let X, Y be set ; :: thesis: for f being Function holds (Y |` f) | X is PartFunc of X,Y
let f be Function; :: thesis: (Y |` f) | X is PartFunc of X,Y
(Y |` f) | X = Y |` (f | X) by RELAT_1:109;
then ( dom ((Y |` f) | X) c= X & rng ((Y |` f) | X) c= Y ) by RELAT_1:58, RELAT_1:85;
hence (Y |` f) | X is PartFunc of X,Y by RELSET_1:4; :: thesis: verum