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

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