let T be 1-sorted ; :: thesis: for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )
let S be non empty 1-sorted ; :: thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )
let f be Function of T,S; :: thesis: ( rng f = [#] S & f is one-to-one implies ( dom (f ") = [#] S & rng (f ") = [#] T ) )
assume that
A1: rng f = [#] S and
A2: f is one-to-one ; :: thesis: ( dom (f ") = [#] S & rng (f ") = [#] T )
A3: f is onto by A1, FUNCT_2:def 3;
hence dom (f ") = dom (f ") by A2, Def4
.= [#] S by A1, A2, FUNCT_1:32 ;
:: thesis: rng (f ") = [#] T
thus rng (f ") = rng (f ") by A2, A3, Def4
.= dom f by A2, FUNCT_1:33
.= [#] T by FUNCT_2:def 1 ; :: thesis: verum