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
( dom (f | Z) c= Z & rng (f | Z) c= Y ) by RELAT_1:58, RELAT_1:def 19;
hence f | Z is PartFunc of Z,Y by RELSET_1:4; :: thesis: verum