theorem Th40: :: YELLOW18:40

for C being concrete category
for a, b being Object of C st <^a,b^> <> {} & <^b,a^> <> {} holds
for f being Morphism of a,b st f is iso holds
( f is one-to-one & rng f = the_carrier_of b ) by ALTCAT_3:5, Th38, Th39;