let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & f is invertible holds
( f is monic & f is epi )
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & f is invertible holds
( f is monic & f is epi )
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & f is invertible implies ( f is monic & f is epi ) )
assume that
A1: Hom (a,b) <> {} and
A2: f is invertible ; :: thesis: ( f is monic & f is epi )
consider k being Morphism of b,a such that
A3: f * k = id b and
A4: k * f = id a by A1, A2, Th70;
A5: Hom (b,a) <> {} by A1, A2, Th70;

now

let c be Object of C; :: thesis: for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds
g = h
let g, h be Morphism of c,a; :: thesis: ( Hom (c,a) <> {} & f * g = f * h implies g = h )
assume that
A6: Hom (c,a) <> {} and
A7: f * g = f * h ; :: thesis: g = h
g = (k * f) * g by A4, A6, Th57
.= k * (f * h) by A1, A5, A6, A7, Th54
.= (id a) * h by A1, A5, A4, A6, Th54 ;
hence g = h by A6, Th57; :: thesis: verum

end;

hence f is monic by A1, Th60; :: thesis: f is epi

now

let c be Object of C; :: thesis: for g, h being Morphism of b,c st Hom (b,c) <> {} & g * f = h * f holds
g = h
let g, h be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} & g * f = h * f implies g = h )
assume that
A8: Hom (b,c) <> {} and
A9: g * f = h * f ; :: thesis: g = h
g = g * (f * k) by A3, A8, Th58
.= (h * f) * k by A1, A5, A8, A9, Th54
.= h * (id b) by A1, A5, A3, A8, Th54 ;
hence g = h by A8, Th58; :: thesis: verum

end;

hence f is epi by A1, Th65; :: thesis: verum