let C be Category; :: thesis: for f being Morphism of C st f is retraction holds
f is epi
let f be Morphism of C; :: thesis: ( f is retraction implies f is epi )
given g being Morphism of C such that A1: cod g = dom f and
A2: f * g = id (cod f) ; :: according to CAT_3:def 8 :: thesis: f is epi
let p1 be Morphism of C; :: according to CAT_1:def 8 :: thesis: for b₁ being Element of the carrier' of C holds
( not dom p1 = cod f or not dom b₁ = cod f or not cod p1 = cod b₁ or not p1 * f = b₁ * f or p1 = b₁ )
let p2 be Morphism of C; :: thesis: ( not dom p1 = cod f or not dom p2 = cod f or not cod p1 = cod p2 or not p1 * f = p2 * f or p1 = p2 )
assume that
A3: dom p1 = cod f and
A4: dom p2 = cod f and
cod p1 = cod p2 and
A5: p1 * f = p2 * f ; :: thesis: p1 = p2
thus p1 = p1 * (f * g) by A2, A3, CAT_1:22
.= (p2 * f) * g by A1, A3, A5, CAT_1:18
.= p2 * (f * g) by A1, A4, CAT_1:18
.= p2 by A2, A4, CAT_1:22 ; :: thesis: verum