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

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