let C be Category; :: thesis: for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let a, b, c be Object of C; :: thesis: for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
let g be Morphism of b,c; :: thesis: ( Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi implies g is epi )
assume that
A1: Hom (a,b) <> {} and
A2: Hom (b,c) <> {} and
A3: g * f is epi ; :: thesis: g is epi
now :: thesis: for d being Object of C
for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * g = h2 * g holds
h1 = h2
let d be Object of C; :: thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * g = h2 * g holds
h1 = h2
let h1, h2 be Morphism of c,d; :: thesis: ( Hom (c,d) <> {} & h1 * g = h2 * g implies h1 = h2 )
assume A4: Hom (c,d) <> {} ; :: thesis: ( h1 * g = h2 * g implies h1 = h2 )
then ( h1 * (g * f) = (h1 * g) * f & h2 * (g * f) = (h2 * g) * f ) by A1, A2, Th21;
hence ( h1 * g = h2 * g implies h1 = h2 ) by A3, A4; :: thesis: verum
end;
hence g is epi by A2; :: thesis: verum