let X, Y, Z be set ; :: thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds
f | Z is Function of Z,Y
let f be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) & Z c= X implies f | Z is Function of Z,Y )
assume that
A1: ( Y = {} implies X = {} ) and
A2: Z c= X ; :: thesis: f | Z is Function of Z,Y
dom f = X by A1, Def1;
then A3: Z = dom (f | Z) by A2, RELAT_1:62;
rng (f | Z) c= Y ;
then reconsider R = f | Z as Relation of Z,Y by A3, RELSET_1:4;
R is quasi_total

proof

per cases ( Y <> {} or Y = {} ) ;
:: according to FUNCT_2:def 1

case Y <> {} ; :: thesis: Z = dom R

dom f = X by A1, Def1;
hence Z = dom R by A2, RELAT_1:62; :: thesis: verum

end;

case Y = {} ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

hence f | Z is Function of Z,Y ; :: thesis: verum