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: [#] T = the carrier of T ;
assume A2: ( 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 A3: rng f = the carrier of T by FUNCT_2:def 3;
then ( dom f = the carrier of S & rng (f " ) = [#] S ) by A2, A1, FUNCT_2:def 1, TOPS_2:62;
hence ( f * (f " ) = id T & (f " ) * f = id S & f " is one-to-one & f " is onto ) by A2, A3, A1, FUNCT_2:def 3, TOPS_2:63, TOPS_2:65; :: thesis: verum