let X, Y be set ; :: thesis: for f being Function of X,Y st f is bijective holds
f " is Function of Y,X
let f be Function of X,Y; :: thesis: ( f is bijective implies f " is Function of Y,X )
assume A1: f is bijective ; :: thesis: f " is Function of Y,X
then rng f = Y by FUNCT_2:def 3;
hence f " is Function of Y,X by A1, FUNCT_2:25; :: thesis: verum