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: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