let C be composable with_identities CategoryStr ; :: thesis: for a, b being Object of C

for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds

f1 is epimorphism

let a, b be Object of C; :: thesis: for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds

f1 is epimorphism

let f1 be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & f1 is identity implies f1 is epimorphism )

assume A1: Hom (a,b) <> {} ; :: thesis: ( not f1 is identity or f1 is epimorphism )

assume A2: f1 is identity ; :: thesis: f1 is epimorphism

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 * f1 = g2 * f1 holds

g1 = g2

let c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for g1, g2 being Morphism of b,c st g1 * f1 = g2 * f1 holds

g1 = g2 )

assume A3: Hom (b,c) <> {} ; :: thesis: for g1, g2 being Morphism of b,c st g1 * f1 = g2 * f1 holds

g1 = g2

let g1, g2 be Morphism of b,c; :: thesis: ( g1 * f1 = g2 * f1 implies g1 = g2 )

assume A4: g1 * f1 = g2 * f1 ; :: thesis: g1 = g2

thus g1 = g1 * f1 by A3, A1, A2, Th24

.= g2 by A3, A1, A4, A2, Th24 ; :: thesis: verum

for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds

f1 is epimorphism

let a, b be Object of C; :: thesis: for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds

f1 is epimorphism

let f1 be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & f1 is identity implies f1 is epimorphism )

assume A1: Hom (a,b) <> {} ; :: thesis: ( not f1 is identity or f1 is epimorphism )

assume A2: f1 is identity ; :: thesis: f1 is epimorphism

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 * f1 = g2 * f1 holds

g1 = g2

let c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for g1, g2 being Morphism of b,c st g1 * f1 = g2 * f1 holds

g1 = g2 )

assume A3: Hom (b,c) <> {} ; :: thesis: for g1, g2 being Morphism of b,c st g1 * f1 = g2 * f1 holds

g1 = g2

let g1, g2 be Morphism of b,c; :: thesis: ( g1 * f1 = g2 * f1 implies g1 = g2 )

assume A4: g1 * f1 = g2 * f1 ; :: thesis: g1 = g2

thus g1 = g1 * f1 by A3, A1, A2, Th24

.= g2 by A3, A1, A4, A2, Th24 ; :: thesis: verum