let S be 1-sorted ; :: thesis: for T being non empty 1-sorted

for f being Function of S,T st f is bijective holds

f " is bijective

let T be non empty 1-sorted ; :: thesis: for f being Function of S,T st f is bijective holds

f " is bijective

let f be Function of S,T; :: thesis: ( f is bijective implies f " is bijective )

assume A1: f is bijective ; :: thesis: f " is bijective

then A2: rng f = [#] T by FUNCT_2:def 3;

then rng (f ") = [#] S by A1, TOPS_2:49;

then A3: f " is onto by FUNCT_2:def 3;

f " is one-to-one by A1, A2, TOPS_2:50;

hence f " is bijective by A3; :: thesis: verum

for f being Function of S,T st f is bijective holds

f " is bijective

let T be non empty 1-sorted ; :: thesis: for f being Function of S,T st f is bijective holds

f " is bijective

let f be Function of S,T; :: thesis: ( f is bijective implies f " is bijective )

assume A1: f is bijective ; :: thesis: f " is bijective

then A2: rng f = [#] T by FUNCT_2:def 3;

then rng (f ") = [#] S by A1, TOPS_2:49;

then A3: f " is onto by FUNCT_2:def 3;

f " is one-to-one by A1, A2, TOPS_2:50;

hence f " is bijective by A3; :: thesis: verum