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_{1}[ 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_{1}[x,y] )

A9: for x being object st x in the carrier of (OrdC 2) holds

S_{1}[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

for g1, g2 being morphism of (OrdC 2) st g1 |> g2 holds

( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

take F ; :: thesis: for g being morphism of (OrdC 2) st not g is identity holds

F . g = f

let g be morphism of (OrdC 2); :: thesis: ( not g is identity implies F . g = f )

assume A37: not g is identity ; :: thesis: F . g = f

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: verum

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

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

proof

consider F being Function of the carrier of (OrdC 2), the carrier of C such that
let x be object ; :: thesis: ( x in the carrier of (OrdC 2) implies ex y being object st

( y in the carrier of C & S_{1}[x,y] ) )

assume x in the carrier of (OrdC 2) ; :: thesis: ex y being object st

( y in the carrier of C & S_{1}[x,y] )

then A5: x in {(dom f1),(cod f1),f1} by CAT_6:def 1, A2;

end;( y in the carrier of C & S

assume x in the carrier of (OrdC 2) ; :: thesis: ex y being object st

( y in the carrier of C & S

then A5: x in {(dom f1),(cod f1),f1} by CAT_6:def 1, A2;

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

end;

suppose A6:
x = dom f1
; :: thesis: ex y being object st

( y in the carrier of C & S_{1}[x,y] )

( y in the carrier of C & S

reconsider y = dom f as object ;

take y ; :: thesis: ( y in the carrier of C & S_{1}[x,y] )

y in Ob C ;

then y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A6, A3, ZFMISC_1:def 5; :: thesis: verum

end;take y ; :: thesis: ( y in the carrier of C & S

y in Ob C ;

then y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S

thus S

suppose A7:
x = cod f1
; :: thesis: ex y being object st

( y in the carrier of C & S_{1}[x,y] )

( y in the carrier of C & S

reconsider y = cod f as object ;

take y ; :: thesis: ( y in the carrier of C & S_{1}[x,y] )

y in Ob C ;

then y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A7, A3, ZFMISC_1:def 5; :: thesis: verum

end;take y ; :: thesis: ( y in the carrier of C & S

y in Ob C ;

then y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S

thus S

suppose A8:
x = f1
; :: thesis: ex y being object st

( y in the carrier of C & S_{1}[x,y] )

( y in the carrier of C & S

reconsider y = f as object ;

take y ; :: thesis: ( y in the carrier of C & S_{1}[x,y] )

y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A8, A3, ZFMISC_1:def 5; :: thesis: verum

end;take y ; :: thesis: ( y in the carrier of C & S

y in Mor C ;

hence y in the carrier of C by CAT_6:def 1; :: thesis: S

thus S

A9: for x being object st x in the carrier of (OrdC 2) holds

S

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

then A12:
F is identity-preserving
by CAT_6:def 22;
let g be morphism of (OrdC 2); :: thesis: ( g is identity implies F . g is identity )

assume A10: g is identity ; :: thesis: F . g is identity

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_{1}[x,F . x]
by A9;

hence F . g is identity by A11, CAT_6:22, A2, A1, A10, ENUMSET1:def 1; :: thesis: verum

end;assume A10: g is identity ; :: thesis: F . g is identity

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

hence F . g is identity by A11, CAT_6:22, A2, A1, A10, ENUMSET1:def 1; :: thesis: verum

for g1, g2 being morphism of (OrdC 2) st g1 |> g2 holds

( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

proof

then reconsider F = F as covariant Functor of (OrdC 2),C by A12, CAT_6:def 23, CAT_6:def 25;
let g1, g2 be morphism of (OrdC 2); :: thesis: ( g1 |> g2 implies ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) )

assume A13: g1 |> g2 ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

A14: for g being morphism of (OrdC 2) st g = dom f1 holds

F . g = dom f

F . g = cod f

F . g = f

end;assume A13: g1 |> g2 ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

A14: for g being morphism of (OrdC 2) st g = dom f1 holds

F . g = dom f

proof

A17:
for g being morphism of (OrdC 2) st g = cod f1 holds
let g be morphism of (OrdC 2); :: thesis: ( g = dom f1 implies F . g = dom f )

assume A15: g = dom f1 ; :: thesis: F . g = dom f

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: verum

end;assume A15: g = dom f1 ; :: thesis: F . g = dom f

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: verum

F . g = cod f

proof

A20:
for g being morphism of (OrdC 2) st g = f1 holds
let g be morphism of (OrdC 2); :: thesis: ( g = cod f1 implies F . g = cod f )

assume A18: g = cod f1 ; :: thesis: F . g = cod f

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: verum

end;assume A18: g = cod f1 ; :: thesis: F . g = cod f

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: verum

F . g = f

proof

let g be morphism of (OrdC 2); :: thesis: ( g = f1 implies F . g = f )

assume A21: g = f1 ; :: thesis: F . g = f

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: verum

end;assume A21: g = f1 ; :: thesis: F . g = f

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: verum

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

end;

suppose A23:
( g1 = dom f1 & g2 = dom f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A24:
( F . g1 = dom f & F . g2 = dom f )
by A14;

hence A25: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A23, A13, CAT_6:23

.= (F . g1) (*) (F . g2) by A25, A24, CAT_6:23 ; :: thesis: verum

end;hence A25: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A23, A13, CAT_6:23

.= (F . g1) (*) (F . g2) by A25, A24, CAT_6:23 ; :: thesis: verum

suppose A26:
( g1 = dom f1 & g2 = cod f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

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: verum

end;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: verum

suppose A27:
( g1 = dom f1 & g2 = f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

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: verum

end;hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A27, A3, ZFMISC_1:def 5; :: thesis: verum

suppose A28:
( g1 = cod f1 & g2 = dom f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

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: verum

end;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: verum

suppose A29:
( g1 = cod f1 & g2 = cod f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A30:
( F . g1 = cod f & F . g2 = cod f )
by A17;

hence A31: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A29, A13, CAT_6:23

.= (F . g1) (*) (F . g2) by A31, A30, CAT_6:23 ; :: thesis: verum

end;hence A31: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A29, A13, CAT_6:23

.= (F . g1) (*) (F . g2) by A31, A30, CAT_6:23 ; :: thesis: verum

suppose A32:
( g1 = cod f1 & g2 = f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A33:
( F . g1 = cod f & F . g2 = f )
by A17, A20;

hence F . g1 |> F . g2 by Th9; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g2 by A32, Th9

.= (F . g1) (*) (F . g2) by A33, Th9 ; :: thesis: verum

end;hence F . g1 |> F . g2 by Th9; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g2 by A32, Th9

.= (F . g1) (*) (F . g2) by A33, Th9 ; :: thesis: verum

suppose A34:
( g1 = f1 & g2 = dom f1 )
; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A35:
( F . g1 = f & F . g2 = dom f )
by A14, A20;

hence F . g1 |> F . g2 by Th8; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A34, Th8

.= (F . g1) (*) (F . g2) by A35, Th8 ; :: thesis: verum

end;hence F . g1 |> F . g2 by Th8; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)

thus F . (g1 (*) g2) = F . g1 by A34, Th8

.= (F . g1) (*) (F . g2) by A35, Th8 ; :: thesis: verum

take F ; :: thesis: for g being morphism of (OrdC 2) st not g is identity holds

F . g = f

let g be morphism of (OrdC 2); :: thesis: ( not g is identity implies F . g = f )

assume A37: not g is identity ; :: thesis: F . g = f

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: verum