let C be composable with_identities CategoryStr ; :: thesis: for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & b is initial holds
f is epimorphism
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & b is initial holds
f is epimorphism
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & b is initial implies f is epimorphism )
assume that
A1: Hom (a,b) <> {} and
A2: b is initial ; :: thesis: f is epimorphism

now :: thesis: for c being Object of C st Hom (b,c) <> {} holds
for g, h being Morphism of b,c st g * f = h * f holds
g = h

let c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for g, h being Morphism of b,c st g * f = h * f holds
g = h )
assume Hom (b,c) <> {} ; :: thesis: for g, h being Morphism of b,c st g * f = h * f holds
g = h
let g, h be Morphism of b,c; :: thesis: ( g * f = h * f implies g = h )
assume g * f = h * f ; :: thesis: g = h
consider f1 being Morphism of b,c such that
A3: for g1 being Morphism of b,c holds f1 = g1 by A2;
f1 = g by A3;
hence g = h by A3; :: thesis: verum

end;

hence f is epimorphism by A1, CAT_7:def 6; :: thesis: verum