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

per cases ( g = dom f1 or g = cod f1 or g = f1 ) by A2, ENUMSET1:def 1;

suppose g = dom f1 ; :: thesis: (MORPHISM f) . g = f

hence (MORPHISM f) . g = (MORPHISM f) . (dom f1) by CAT_6:def 21
.= dom ((MORPHISM f) . f1) by CAT_6:32
.= dom f by A2, Def16
.= f by A1, Th6 ;
:: thesis: verum

end;

suppose g = cod f1 ; :: thesis: (MORPHISM f) . g = f

hence (MORPHISM f) . g = (MORPHISM f) . (cod f1) by CAT_6:def 21
.= cod ((MORPHISM f) . f1) by CAT_6:32
.= cod f by A2, Def16
.= f by A1, Th6 ;
:: thesis: verum

end;

suppose g = f1 ; :: thesis: (MORPHISM f) . g = f

hence (MORPHISM f) . g = f by A2, Def16; :: thesis: verum

end;

end;