let C be non empty category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st f is retraction holds
f is epimorphism
let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is retraction holds
f is epimorphism
let f be Morphism of a,b; :: thesis: ( f is retraction implies f is epimorphism )
assume A1: f is retraction ; :: thesis: f is epimorphism
then consider g being Morphism of b,a such that
A2: f * g = id- b ;
thus Hom (a,b) <> {} by A1; :: according to CAT_7:def 6 :: thesis: for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2
let c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 )
assume A3: Hom (b,c) <> {} ; :: thesis: for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2
let g1, g2 be Morphism of b,c; :: thesis: ( g1 * f = g2 * f implies g1 = g2 )
assume A4: g1 * f = g2 * f ; :: thesis: g1 = g2
A5: g1 * (f * g) = (g1 * f) * g by A1, A3, Th23
.= g2 * (f * g) by A1, A4, A3, Th23 ;
thus g1 = g1 * (f * g) by A3, A2, Th18
.= g2 by A5, A3, A2, Th18 ; :: thesis: verum