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