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