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 f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 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 f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 is epimorphism
let f1 be Morphism of a,b; :: thesis: for f2 being Morphism of b,c st f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} holds
f2 is epimorphism
let f2 be Morphism of b,c; :: thesis: ( f2 * f1 is epimorphism & Hom (a,b) <> {} & Hom (b,c) <> {} implies f2 is epimorphism )
assume A1: f2 * f1 is epimorphism ; :: thesis: ( not Hom (a,b) <> {} or not Hom (b,c) <> {} or f2 is epimorphism )
assume A2: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ; :: thesis: f2 is epimorphism
thus Hom (b,c) <> {} by A2; :: 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 = g2 * f2 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 = g2 * f2 holds
g1 = g2 )
assume A3: Hom (c,d) <> {} ; :: thesis: for g1, g2 being Morphism of c,d st g1 * f2 = g2 * f2 holds
g1 = g2
let g1, g2 be Morphism of c,d; :: thesis: ( g1 * f2 = g2 * f2 implies g1 = g2 )
assume A4: g1 * f2 = g2 * f2 ; :: thesis: g1 = g2
g1 * (f2 * f1) = (g1 * f2) * f1 by A2, A3, Th23
.= g2 * (f2 * f1) by A2, A4, A3, Th23 ;
hence g1 = g2 by A1, A3; :: thesis: verum