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;

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;

end;

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;.= dom ((MORPHISM f) . f1) by CAT_6:32

.= dom f by A2, Def16

.= f by A1, Th6 ;

:: thesis: verum