let T, S be 1-sorted ; :: thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) )
let f be Function of T,S; :: thesis: ( rng f = [#] S & f is one-to-one implies ( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) ) )
assume A1: ( rng f = [#] S & f is one-to-one ) ; :: thesis: ( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) )
then ( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) ) by FUNCT_1:61;
hence ( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) ) by A1, Def4; :: thesis: verum