let C be non empty category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st f is isomorphism holds
( f is monomorphism & f is epimorphism )
let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is isomorphism holds
( f is monomorphism & f is epimorphism )
let f be Morphism of a,b; :: thesis: ( f is isomorphism implies ( f is monomorphism & f is epimorphism ) )
assume A1: f is isomorphism ; :: thesis: ( f is monomorphism & f is epimorphism )
f is section_ by A1;
hence f is monomorphism by Th28; :: thesis: f is epimorphism
f is retraction by A1;
hence f is epimorphism by Th32; :: thesis: verum