let X, Y, Z be set ; :: thesis: for f being Function of [:X,Y:],Z st Z <> {} holds
~ f is Function of [:Y,X:],Z
let f be Function of [:X,Y:],Z; :: thesis: ( Z <> {} implies ~ f is Function of [:Y,X:],Z )
assume A1: Z <> {} ; :: thesis: ~ f is Function of [:Y,X:],Z
then ( dom f = [:X,Y:] & rng f c= Z ) by FUNCT_2:def 1;
then ( [:Y,X:] = dom (~ f) & rng (~ f) c= Z ) by Th47, Th48;
then reconsider R = ~ f as Relation of [:Y,X:],Z by RELSET_1:11;
R is quasi_total

proof

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

case ( Z = {} implies [:Y,X:] = {} ) ; :: thesis: [:Y,X:] = dom R

( dom f = [:X,Y:] & rng f c= Z ) by A1, FUNCT_2:def 1;
hence [:Y,X:] = dom R by Th47; :: thesis: verum

end;

case ( Z = {} & [:Y,X:] <> {} ) ; :: thesis: R = {}

hence R = {} ; :: thesis: verum

end;

end;

end;

hence ~ f is Function of [:Y,X:],Z ; :: thesis: verum