let X, Y, Z be set ; :: thesis: for f being PartFunc of X,Y holds Z | f is PartFunc of X,Z
let f be PartFunc of X,Y; :: thesis: Z | f is PartFunc of X,Z
( dom (Z | f) c= X & rng (Z | f) c= Z ) by RELAT_1:116;
hence Z | f is PartFunc of X,Z by RELSET_1:11; :: thesis: verum