let X, Y, Z be set ; :: thesis: for f being Function of [:X,Y:],Z holds ~ f is Function of [:Y,X:],Z
let f be Function of [:X,Y:],Z; :: thesis: ~ f is Function of [:Y,X:],Z

per cases ( Z = {} or Z <> {} ) ;

suppose A1: Z = {} ; :: thesis: ~ f is Function of [:Y,X:],Z

then reconsider f = f as empty set ;
~ f = {} ;
hence ~ f is Function of [:Y,X:],Z by A1, FUNCT_2:130; :: thesis: verum

end;

suppose A1: Z <> {} ; :: thesis: ~ f is Function of [:Y,X:],Z

reconsider R = ~ f as Relation of [:Y,X:],Z ;
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

end;

end;