let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st f is retraction holds
f is epi

let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is retraction holds
f is epi

let f be Morphism of a,b; :: thesis: ( f is retraction implies f is epi )
assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of b,a holds not f * g = id b or f is epi )
given g being Morphism of b,a such that A2: f * g = id b ; :: thesis: f is epi
thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 15 :: thesis: for b1 being Element of the carrier of C holds
( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds
( not b2 * f = b3 * f or b2 = b3 ) )

let c be Object of C; :: thesis: ( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 ) )

assume A3: Hom (b,c) <> {} ; :: thesis: for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 )

let p1, p2 be Morphism of b,c; :: thesis: ( not p1 * f = p2 * f or p1 = p2 )
assume A4: p1 * f = p2 * f ; :: thesis: p1 = p2
thus p1 = p1 * (f * g) by
.= (p2 * f) * g by
.= p2 * (f * g) by
.= p2 by ; :: thesis: verum