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) <> {} & a is terminal holds
f is monomorphism
let a, b be Object of C; :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monomorphism
let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & a is terminal implies f is monomorphism )
assume that
A1: Hom (a,b) <> {} and
A2: a is terminal ; :: thesis: f is monomorphism

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

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

end;

hence f is monomorphism by A1, CAT_7:def 5; :: thesis: verum