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

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