let Y, X 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:140;
then ( dom ((Y | f) | X) c= X & rng ((Y | f) | X) c= Y ) by RELAT_1:87, RELAT_1:116;
hence (Y | f) | X is PartFunc of X,Y by RELSET_1:11; :: thesis: verum