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:91;
rng (f | Z) c= Y ;
then reconsider R = f | Z as Relation of Z,Y by A3, RELSET_1:11;
R is quasi_total

proof

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

case ( Y = {} implies Z = {} ) ; :: thesis: Z = dom R

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

end;

case ( Y = {} & Z <> {} ) ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

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