let C be composable with_identities CategoryStr ; for a, b being Object of C
for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds
f1 is monomorphism
let a, b be Object of C; for f1 being Morphism of a,b st Hom (a,b) <> {} & f1 is identity holds
f1 is monomorphism
let f1 be Morphism of a,b; ( Hom (a,b) <> {} & f1 is identity implies f1 is monomorphism )
assume A1:
Hom (a,b) <> {}
; ( not f1 is identity or f1 is monomorphism )
assume A2:
f1 is identity
; f1 is monomorphism
thus
Hom (a,b) <> {}
by A1; CAT_7:def 5 for c being Object of C st Hom (c,a) <> {} holds
for g1, g2 being Morphism of c,a st f1 * g1 = f1 * g2 holds
g1 = g2
let c be Object of C; ( Hom (c,a) <> {} implies for g1, g2 being Morphism of c,a st f1 * g1 = f1 * g2 holds
g1 = g2 )
assume A3:
Hom (c,a) <> {}
; for g1, g2 being Morphism of c,a st f1 * g1 = f1 * g2 holds
g1 = g2
let g1, g2 be Morphism of c,a; ( f1 * g1 = f1 * g2 implies g1 = g2 )
assume A4:
f1 * g1 = f1 * g2
; g1 = g2
thus g1 =
f1 * g1
by A3, A1, A2, Th24
.=
g2
by A3, A1, A4, A2, Th24
; verum