let C be category; 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; 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; 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; ( f1 is epimorphism & f2 is epimorphism implies f2 * f1 is epimorphism )
assume A1:
f1 is epimorphism
; ( not f2 is epimorphism or f2 * f1 is epimorphism )
assume A2:
f2 is epimorphism
; f2 * f1 is epimorphism
hence
Hom (a,c) <> {}
by A1, Th22; CAT_7:def 6 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; ( 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) <> {}
; 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; ( g1 * (f2 * f1) = g2 * (f2 * f1) implies g1 = g2 )
assume A4:
g1 * (f2 * f1) = g2 * (f2 * f1)
; 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; verum