let S, T be non empty 1-sorted ; :: thesis: for f being Function of S,T st f is one-to-one & f is onto holds
( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto )
let f be Function of S,T; :: thesis: ( f is one-to-one & f is onto implies ( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto ) )
A1: dom f = the carrier of S by FUNCT_2:def 1;
assume ( f is one-to-one & f is onto ) ; :: thesis: ( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto )
then ( f is one-to-one & rng f = the carrier of T & [#] T = the carrier of T ) by FUNCT_2:def 3;
then ( f * (f " ) = id the carrier of T & (f " ) * f = id the carrier of S & rng (f " ) = [#] S & f " is one-to-one & [#] S = the carrier of S ) by A1, TOPS_2:62, TOPS_2:63, TOPS_2:65;
hence ( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto ) by FUNCT_2:def 3; :: thesis: verum