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

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