let X, Y, Z be non empty set ; :: thesis: for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y
let f be PartFunc of X,Y; :: thesis: ( Z c= dom f implies f | Z is Function of Z,Y )
rng f c= Y ;
then f is Function of (dom f),Y by FUNCT_2:2;
hence ( Z c= dom f implies f | Z is Function of Z,Y ) by FUNCT_2:32; :: thesis: verum