let C be non empty category; :: thesis: for F1, F2 being covariant Functor of (OrdC 2),C
for f being morphism of (OrdC 2) st not f is identity & F1 . f = F2 . f holds
F1 = F2
let F1, F2 be covariant Functor of (OrdC 2),C; :: thesis: for f being morphism of (OrdC 2) st not f is identity & F1 . f = F2 . f holds
F1 = F2
let f be morphism of (OrdC 2); :: thesis: ( not f is identity & F1 . f = F2 . f implies F1 = F2 )
assume A1: not f is identity ; :: thesis: ( not F1 . f = F2 . f or F1 = F2 )
assume A2: F1 . f = F2 . f ; :: thesis: F1 = F2
A3: dom F1 = the carrier of (OrdC 2) by FUNCT_2:def 1
.= dom F2 by FUNCT_2:def 1 ;
consider f1 being morphism of (OrdC 2) such that
A4: ( 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 CAT_7:39;
A5: ( f = dom f1 or f = cod f1 or f = f1 ) by A4, ENUMSET1:def 1;
for x being object st x in dom F1 holds
F1 . x = F2 . x

proof

let x be object ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume x in dom F1 ; :: thesis: F1 . x = F2 . x
then x in the carrier of (OrdC 2) ;
then A6: x in {(dom f1),(cod f1),f1} by A4, CAT_6:def 1;

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

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

thus F1 . x = dom (F2 . f1) by A2, A5, A1, CAT_6:22, A7, CAT_6:32
.= F2 . x by A7, CAT_6:32 ; :: thesis: verum

end;

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

thus F1 . x = cod (F2 . f1) by A2, A5, A1, CAT_6:22, A8, CAT_6:32
.= F2 . x by A8, CAT_6:32 ; :: thesis: verum

end;

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

thus F1 . x = F2 . f1 by A2, A5, A1, CAT_6:22, A9, CAT_6:def 21
.= F2 . x by A9, CAT_6:def 21 ; :: thesis: verum

end;

end;

end;

hence F1 = F2 by A3, FUNCT_1:2; :: thesis: verum