let C be category; :: thesis: for a, b, c being Object of C

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let a, b, c be Object of C; :: thesis: for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let f2 be Morphism of b,c; :: thesis: ( f1 is epimorphism & f2 is epimorphism implies f2 * f1 is epimorphism )

assume A1: f1 is epimorphism ; :: thesis: ( not f2 is epimorphism or f2 * f1 is epimorphism )

assume A2: f2 is epimorphism ; :: thesis: f2 * f1 is epimorphism

hence Hom (a,c) <> {} by A1, Th22; :: according to CAT_7:def 6 :: thesis: for c being Object of C st Hom (c,c) <> {} holds

for g1, g2 being Morphism of c,c st g1 * (f2 * f1) = g2 * (f2 * f1) holds

g1 = g2

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

g1 = g2 )

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

g1 = g2

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

assume A4: g1 * (f2 * f1) = g2 * (f2 * f1) ; :: thesis: g1 = g2

A5: Hom (b,d) <> {} by A3, A2, Th22;

(g1 * f2) * f1 = g1 * (f2 * f1) by A1, A2, A3, Th23

.= (g2 * f2) * f1 by A4, A1, A2, A3, Th23 ;

hence g1 = g2 by A3, A2, A1, A5; :: thesis: verum

for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let a, b, c be Object of C; :: thesis: for f1 being Morphism of a,b

for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f1 is epimorphism & f2 is epimorphism holds

f2 * f1 is epimorphism

let f2 be Morphism of b,c; :: thesis: ( f1 is epimorphism & f2 is epimorphism implies f2 * f1 is epimorphism )

assume A1: f1 is epimorphism ; :: thesis: ( not f2 is epimorphism or f2 * f1 is epimorphism )

assume A2: f2 is epimorphism ; :: thesis: f2 * f1 is epimorphism

hence Hom (a,c) <> {} by A1, Th22; :: according to CAT_7:def 6 :: thesis: for c being Object of C st Hom (c,c) <> {} holds

for g1, g2 being Morphism of c,c st g1 * (f2 * f1) = g2 * (f2 * f1) holds

g1 = g2

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

g1 = g2 )

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

g1 = g2

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

assume A4: g1 * (f2 * f1) = g2 * (f2 * f1) ; :: thesis: g1 = g2

A5: Hom (b,d) <> {} by A3, A2, Th22;

(g1 * f2) * f1 = g1 * (f2 * f1) by A1, A2, A3, Th23

.= (g2 * f2) * f1 by A4, A1, A2, A3, Th23 ;

hence g1 = g2 by A3, A2, A1, A5; :: thesis: verum