let X, Y, Z be set ; :: thesis: for f being Function of X,Y st ( Y = {} implies X = {} ) & Y c= Z holds
f is Function of X,Z
let f be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) & Y c= Z implies f is Function of X,Z )
assume that
A1: ( Y <> {} or X = {} ) and
A2: Y c= Z ; :: thesis: f is Function of X,Z
reconsider R = f as Relation of X,Z by A2, RELSET_1:17;
R is quasi_total

proof

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

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

thus X = dom R by A1, Def1; :: thesis: verum

end;

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

hence R = {} ; :: thesis: verum

end;

end;

end;

hence f is Function of X,Z ; :: thesis: verum