let C be non empty category; for f1, f2 being morphism of C st MORPHISM f1 = MORPHISM f2 holds
f1 = f2
let f1, f2 be morphism of C; ( MORPHISM f1 = MORPHISM f2 implies f1 = f2 )
assume A1:
MORPHISM f1 = MORPHISM f2
; f1 = f2
consider f being morphism of (OrdC 2) such that
A2:
( not f is identity & Ob (OrdC 2) = {(dom f),(cod f)} & Mor (OrdC 2) = {(dom f),(cod f),f} & dom f, cod f,f are_mutually_distinct )
by CAT_7:39;
thus f1 =
(MORPHISM f1) . f
by A2, CAT_7:def 16
.=
f2
by A1, A2, CAT_7:def 16
; verum