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:85;
hence Z |` f is PartFunc of X,Z by RELSET_1:4; :: thesis: verum