let C be concrete category; :: thesis: 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 )
let a, b be object of C; :: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies for f being Morphism of a,b st f is iso holds
( f is one-to-one & rng f = the_carrier_of b ) )
assume A1: ( <^a,b^> <> {} & <^b,a^> <> {} ) ; :: thesis: for f being Morphism of a,b st f is iso holds
( f is one-to-one & rng f = the_carrier_of b )
let f be Morphism of a,b; :: thesis: ( f is iso implies ( f is one-to-one & rng f = the_carrier_of b ) )
assume f is iso ; :: thesis: ( f is one-to-one & rng f = the_carrier_of b )
then ( f is retraction & f is coretraction ) by ALTCAT_3:5;
hence ( f is one-to-one & rng f = the_carrier_of b ) by A1, Th40, Th41; :: thesis: verum