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 Th46;
rng f c= Z ;
then rng (~ f) c= Z by A2, Th47;
then reconsider R = ~ f as Relation of [:Y,X:],Z by A3, RELSET_1:4;
R is quasi_total

proof

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

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

dom f = [:X,Y:] by A1, FUNCT_2:def 1;
hence [:Y,X:] = dom R by Th46; :: thesis: verum

end;

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

hence R = {} ; :: thesis: verum

end;

end;

end;

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