let F1, F2 be covariant Functor of (OrdC 2),C; :: thesis: ( ( for g being morphism of (OrdC 2) st not g is identity holds
F1 . g = f ) & ( for g being morphism of (OrdC 2) st not g is identity holds
F2 . g = f ) implies F1 = F2 )
assume A40: for g being morphism of (OrdC 2) st not g is identity holds
F1 . g = f ; :: thesis: ( ex g being morphism of (OrdC 2) st
( not g is identity & not F2 . g = f ) or F1 = F2 )
assume A41: for g being morphism of (OrdC 2) st not g is identity holds
F2 . g = f ; :: thesis: F1 = F2
consider f1 being morphism of (OrdC 2) such that
A42: not f1 is identity and
Ob (OrdC 2) = {(dom f1),(cod f1)} and
A43: Mor (OrdC 2) = {(dom f1),(cod f1),f1} by Th39;
for x being object st x in the carrier of (OrdC 2) holds
F1 . x = F2 . x

proof

let x be object ; :: thesis: ( x in the carrier of (OrdC 2) implies F1 . x = F2 . x )
assume x in the carrier of (OrdC 2) ; :: thesis: F1 . x = F2 . x
then A44: x in {(dom f1),(cod f1),f1} by A43, CAT_6:def 1;
A45: F1 . f1 = f by A40, A42
.= F2 . f1 by A41, A42 ;

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

suppose A46: x = dom f1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = dom (F1 . f1) by CAT_6:32
.= F2 . x by A46, A45, CAT_6:32 ;
:: thesis: verum

end;

suppose A47: x = cod f1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = cod (F1 . f1) by CAT_6:32
.= F2 . x by A47, A45, CAT_6:32 ;
:: thesis: verum

end;

suppose A48: x = f1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 . f1 by CAT_6:def 21
.= F2 . x by A45, A48, CAT_6:def 21 ;
:: thesis: verum

end;

end;

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum