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
end;
end;
hence ~ f is Function of [:Y,X:],Z ; :: thesis: verum
end;
end;