let C be non empty category; :: thesis: for f1, f2 being morphism of C st MORPHISM f1 = MORPHISM f2 holds
f1 = f2
let f1, f2 be morphism of C; :: thesis: ( MORPHISM f1 = MORPHISM f2 implies f1 = f2 )
assume A1: MORPHISM f1 = MORPHISM f2 ; :: thesis: 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 ; :: thesis: verum