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 A2: dom f = [:X,Y:] by FUNCT_2:def 1;
then A3: [:Y,X:] = dom (~ f) by Th47;
rng f c= Z ;
then rng (~ f) c= Z by A2, Th48;
then reconsider R = ~ f as Relation of [:Y,X:],Z by A3, 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:] 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