theorem :: TOPS_2:52

for T, S being 1-sorted
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) )