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

now :: thesis: for c being Object of C
for g, h being Morphism of c,a st Hom (c,a) <> {} & f * g = f * h holds
g = h

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, Th23
.= k * (f * h) by A2, A5, A6, A7, Th21
.= (id a) * h by A2, A5, A4, A6, Th21 ;
hence g = h by A6, Th23; :: thesis: verum

end;

hence f is monic by A2; :: thesis: f is epi

now :: thesis: for c being Object of C
for g, h being Morphism of b,c st Hom (b,c) <> {} & g * f = h * f holds
g = h

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, Th24
.= (h * f) * k by A2, A5, A8, A9, Th21
.= h * (id b) by A2, A5, A3, A8, Th21 ;
hence g = h by A8, Th24; :: thesis: verum

end;

hence f is epi by A2; :: thesis: verum