consider f1 being morphism of (OrdC 2) such that
A1: not f1 is identity and
Ob (OrdC 2) = {(dom f1),(cod f1)} and
A2: Mor (OrdC 2) = {(dom f1),(cod f1),f1} and
A3: dom f1, cod f1,f1 are_mutually_distinct by Th39;
defpred S₁[ object , object ] means ( ( $1 = dom f1 implies $2 = dom f ) & ( $1 = cod f1 implies $2 = cod f ) & ( $1 = f1 implies $2 = f ) );
A4: for x being object st x in the carrier of (OrdC 2) holds
ex y being object st
( y in the carrier of C & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of (OrdC 2) ; :: thesis:
then A5: x in {(dom f1),(cod f1),f1} by CAT_6:def 1, A2;

per cases by A5, ENUMSET1:def 1;

suppose A6: x = dom f1 ; :: thesis:

reconsider y = dom f as object ;
take y ; :: thesis:
y in Ob C ;
then y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis:
thus S₁[x,y] by A6, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose A7: x = cod f1 ; :: thesis:

reconsider y = cod f as object ;
take y ; :: thesis:
y in Ob C ;
then y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis:
thus S₁[x,y] by A7, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose A8: x = f1 ; :: thesis:

reconsider y = f as object ;
take y ; :: thesis:
y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis:
thus S₁[x,y] by A8, A3, ZFMISC_1:def 5; :: thesis:

end;

consider F being Function of the carrier of (OrdC 2), the carrier of C such that
A9: for x being object st x in the carrier of (OrdC 2) holds
S₁[x,F . x] from FUNCT_2:sch 1(A4);
reconsider F = F as Functor of (OrdC 2),C ;
for g being morphism of (OrdC 2) st g is identity holds
F . g is identity

proof

let g be morphism of (OrdC 2); :: thesis:
assume A10: g is identity ; :: thesis:
reconsider x = g as object ;
A11: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 2) ;
then x in the carrier of (OrdC 2) by CAT_6:def 1;
then S₁[x,F . x] by A9;
hence F . g is identity by A11, CAT_6:22, A2, A1, A10, ENUMSET1:def 1; :: thesis:

end;

then A12: F is identity-preserving by CAT_6:def 22;
for g1, g2 being morphism of (OrdC 2) st g1 |> g2 holds
( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

proof

let g1, g2 be morphism of (OrdC 2); :: thesis:
assume A13: g1 |> g2 ; :: thesis:
A14: for g being morphism of (OrdC 2) st g = dom f1 holds
F . g = dom f

proof

let g be morphism of (OrdC 2); :: thesis:
assume A15: g = dom f1 ; :: thesis:
reconsider x = g as object ;
A16: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 2) ;
then x in the carrier of (OrdC 2) by CAT_6:def 1;
hence F . g = dom f by A9, A15, A16; :: thesis:

end;

A17: for g being morphism of (OrdC 2) st g = cod f1 holds
F . g = cod f

proof

let g be morphism of (OrdC 2); :: thesis:
assume A18: g = cod f1 ; :: thesis:
reconsider x = g as object ;
A19: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 2) ;
then x in the carrier of (OrdC 2) by CAT_6:def 1;
hence F . g = cod f by A9, A18, A19; :: thesis:

end;

A20: for g being morphism of (OrdC 2) st g = f1 holds
F . g = f

proof

let g be morphism of (OrdC 2); :: thesis:
assume A21: g = f1 ; :: thesis:
reconsider x = g as object ;
A22: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 2) ;
then x in the carrier of (OrdC 2) by CAT_6:def 1;
hence F . g = f by A9, A21, A22; :: thesis:

end;

per cases by A2, ENUMSET1:def 1;

suppose A23: ( g1 = dom f1 & g2 = dom f1 ) ; :: thesis:

then A24: ( F . g1 = dom f & F . g2 = dom f ) by A14;
hence A25: F . g1 |> F . g2 by CAT_6:23; :: thesis:
thus F . (g1 (*) g2) = F . g1 by A23, A13, CAT_6:23
.= (F . g1) (*) (F . g2) by A25, A24, CAT_6:23 ; :: thesis:

end;

suppose A26: ( g1 = dom f1 & g2 = cod f1 ) ; :: thesis:

then ( g1 is identity & g2 is identity ) by CAT_6:22;
then g1 = g2 by A13, Th7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A26, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose A27: ( g1 = dom f1 & g2 = f1 ) ; :: thesis:

then cod f1 = g1 by A13, CAT_6:22, CAT_6:27;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A27, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose A28: ( g1 = cod f1 & g2 = dom f1 ) ; :: thesis:

then ( g1 is identity & g2 is identity ) by CAT_6:22;
then g1 = g2 by A13, Th7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A28, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose A29: ( g1 = cod f1 & g2 = cod f1 ) ; :: thesis:

then A30: ( F . g1 = cod f & F . g2 = cod f ) by A17;
hence A31: F . g1 |> F . g2 by CAT_6:23; :: thesis:
thus F . (g1 (*) g2) = F . g1 by A29, A13, CAT_6:23
.= (F . g1) (*) (F . g2) by A31, A30, CAT_6:23 ; :: thesis:

end;

suppose A32: ( g1 = cod f1 & g2 = f1 ) ; :: thesis:

then A33: ( F . g1 = cod f & F . g2 = f ) by A17, A20;
hence F . g1 |> F . g2 by Th9; :: thesis:
thus F . (g1 (*) g2) = F . g2 by A32, Th9
.= (F . g1) (*) (F . g2) by A33, Th9 ; :: thesis:

end;

suppose A34: ( g1 = f1 & g2 = dom f1 ) ; :: thesis:

then A35: ( F . g1 = f & F . g2 = dom f ) by A14, A20;
hence F . g1 |> F . g2 by Th8; :: thesis:
thus F . (g1 (*) g2) = F . g1 by A34, Th8
.= (F . g1) (*) (F . g2) by A35, Th8 ; :: thesis:

end;

suppose A36: ( g1 = f1 & g2 = cod f1 ) ; :: thesis:

then dom f1 = g2 by A13, CAT_6:22, CAT_6:26;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A36, A3, ZFMISC_1:def 5; :: thesis:

end;

suppose ( g1 = f1 & g2 = f1 ) ; :: thesis:

then dom f1 = cod f1 by A13, Th5;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A3, ZFMISC_1:def 5; :: thesis:

end;

then reconsider F = F as covariant Functor of (OrdC 2),C by A12, CAT_6:def 23, CAT_6:def 25;
take F ; :: thesis:
let g be morphism of (OrdC 2); :: thesis:
assume A37: not g is identity ; :: thesis:
A38: ( g = dom f1 or g = cod f1 or g = f1 ) by A2, ENUMSET1:def 1;
reconsider x = g as object ;
A39: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 2) ;
then x in the carrier of (OrdC 2) by CAT_6:def 1;
hence F . g = f by A9, A38, A39, A37, CAT_6:22; :: thesis: