consider h2, h1 being morphism of (OrdC 3) such that
A2: ( not h2 is identity & not h1 is identity & cod h2 = dom h1 ) and
A3: Ob (OrdC 3) = {(dom h2),(cod h2),(cod h1)} and
A4: Mor (OrdC 3) = {(dom h2),(cod h2),(cod h1),h2,h1,(h1 (*) h2)} and
A5: dom h2, cod h2, cod h1,h2,h1,h1 (*) h2 are_mutually_distinct by Th18;
A6: h1 |> h2 by A2, CAT_7:5;
A7: ex F being covariant Functor of (OrdC 3),C st
for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F . g1 = f1 & F . g2 = f2 )

proof

defpred S₁[ object , object ] means ( ( $1 = dom h2 implies $2 = dom f2 ) & ( $1 = cod h2 implies $2 = cod f2 ) & ( $1 = cod h1 implies $2 = cod f1 ) & ( $1 = h2 implies $2 = f2 ) & ( $1 = h1 implies $2 = f1 ) & ( $1 = h1 (*) h2 implies $2 = f1 (*) f2 ) );
A8: for x being object st x in the carrier of (OrdC 3) holds
ex y being object st
( y in the carrier of C & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of (OrdC 3) implies ex y being object st
( y in the carrier of C & S₁[x,y] ) )
assume x in the carrier of (OrdC 3) ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )
then A9: x in {(dom h2),(cod h2),(cod h1),h2,h1,(h1 (*) h2)} by CAT_6:def 1, A4;

per cases ( x = dom h2 or x = cod h2 or x = cod h1 or x = h2 or x = h1 or x = h1 (*) h2 ) by A9, ENUMSET1:def 4;

suppose A10: x = dom h2 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = dom f2 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[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₁[x,y]
thus S₁[x,y] by A10, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A11: x = cod h2 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = cod f2 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[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₁[x,y]
thus S₁[x,y] by A11, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A12: x = cod h1 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = cod f1 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[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₁[x,y]
thus S₁[x,y] by A12, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A13: x = h2 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = f2 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[x,y] )
y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A13, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A14: x = h1 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = f1 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[x,y] )
y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A14, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A15: x = h1 (*) h2 ; :: thesis: ex y being object st
( y in the carrier of C & S₁[x,y] )

reconsider y = f1 (*) f2 as object ;
take y ; :: thesis: ( y in the carrier of C & S₁[x,y] )
y in Mor C ;
hence y in the carrier of C by CAT_6:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A15, A5, ZFMISC_1:def 8; :: thesis: verum

end;

end;

end;

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

proof

let g be morphism of (OrdC 3); :: thesis: ( g is identity implies F . g is identity )
assume A17: g is identity ; :: thesis: F . g is identity
reconsider x = g as object ;
A18: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
then A19: S₁[x,F . x] by A16;
g is Object of (OrdC 3) by A17, CAT_6:22;
hence F . g is identity by A19, A18, CAT_6:22, A3, ENUMSET1:def 1; :: thesis: verum

end;

then A20: F is identity-preserving by CAT_6:def 22;
A21: for g being morphism of (OrdC 3) st g = h2 holds
F . g = f2

proof

let g be morphism of (OrdC 3); :: thesis: ( g = h2 implies F . g = f2 )
assume A22: g = h2 ; :: thesis: F . g = f2
reconsider x = g as object ;
A23: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = f2 by A16, A22, A23; :: thesis: verum

end;

A24: for g being morphism of (OrdC 3) st g = h1 holds
F . g = f1

proof

let g be morphism of (OrdC 3); :: thesis: ( g = h1 implies F . g = f1 )
assume A25: g = h1 ; :: thesis: F . g = f1
reconsider x = g as object ;
A26: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = f1 by A16, A25, A26; :: thesis: verum

end;

for g1, g2 being morphism of (OrdC 3) st g1 |> g2 holds
( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

proof

let g1, g2 be morphism of (OrdC 3); :: thesis: ( g1 |> g2 implies ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) )
assume A27: g1 |> g2 ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )
A28: for g being morphism of (OrdC 3) st g = dom h2 holds
F . g = dom f2

proof

let g be morphism of (OrdC 3); :: thesis: ( g = dom h2 implies F . g = dom f2 )
assume A29: g = dom h2 ; :: thesis: F . g = dom f2
reconsider x = g as object ;
A30: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = dom f2 by A16, A29, A30; :: thesis: verum

end;

A31: for g being morphism of (OrdC 3) st g = cod h2 holds
F . g = cod f2

proof

let g be morphism of (OrdC 3); :: thesis: ( g = cod h2 implies F . g = cod f2 )
assume A32: g = cod h2 ; :: thesis: F . g = cod f2
reconsider x = g as object ;
A33: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = cod f2 by A16, A32, A33; :: thesis: verum

end;

A34: for g being morphism of (OrdC 3) st g = cod h1 holds
F . g = cod f1

proof

let g be morphism of (OrdC 3); :: thesis: ( g = cod h1 implies F . g = cod f1 )
assume A35: g = cod h1 ; :: thesis: F . g = cod f1
reconsider x = g as object ;
A36: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = cod f1 by A16, A35, A36; :: thesis: verum

end;

A37: for g being morphism of (OrdC 3) st g = h1 (*) h2 holds
F . g = f1 (*) f2

proof

let g be morphism of (OrdC 3); :: thesis: ( g = h1 (*) h2 implies F . g = f1 (*) f2 )
assume A38: g = h1 (*) h2 ; :: thesis: F . g = f1 (*) f2
reconsider x = g as object ;
A39: F . x = F . g by CAT_6:def 21;
g in Mor (OrdC 3) ;
then x in the carrier of (OrdC 3) by CAT_6:def 1;
hence F . g = f1 (*) f2 by A16, A38, A39; :: thesis: verum

end;

per cases ( ( g1 = dom h2 & g2 = dom h2 ) or ( g1 = dom h2 & g2 = cod h2 ) or ( g1 = dom h2 & g2 = cod h1 ) or ( g1 = dom h2 & g2 = h2 ) or ( g1 = dom h2 & g2 = h1 ) or ( g1 = dom h2 & g2 = h1 (*) h2 ) or ( g1 = cod h2 & g2 = dom h2 ) or ( g1 = cod h2 & g2 = cod h2 ) or ( g1 = cod h2 & g2 = cod h1 ) or ( g1 = cod h2 & g2 = h2 ) or ( g1 = cod h2 & g2 = h1 ) or ( g1 = cod h2 & g2 = h1 (*) h2 ) or ( g1 = cod h1 & g2 = dom h2 ) or ( g1 = cod h1 & g2 = cod h2 ) or ( g1 = cod h1 & g2 = cod h1 ) or ( g1 = cod h1 & g2 = h2 ) or ( g1 = cod h1 & g2 = h1 ) or ( g1 = cod h1 & g2 = h1 (*) h2 ) or ( g1 = h2 & g2 = dom h2 ) or ( g1 = h2 & g2 = cod h2 ) or ( g1 = h2 & g2 = cod h1 ) or ( g1 = h2 & g2 = h2 ) or ( g1 = h2 & g2 = h1 ) or ( g1 = h2 & g2 = h1 (*) h2 ) or ( g1 = h1 & g2 = dom h2 ) or ( g1 = h1 & g2 = cod h2 ) or ( g1 = h1 & g2 = cod h1 ) or ( g1 = h1 & g2 = h2 ) or ( g1 = h1 & g2 = h1 ) or ( g1 = h1 & g2 = h1 (*) h2 ) or ( g1 = h1 (*) h2 & g2 = dom h2 ) or ( g1 = h1 (*) h2 & g2 = cod h2 ) or ( g1 = h1 (*) h2 & g2 = cod h1 ) or ( g1 = h1 (*) h2 & g2 = h2 ) or ( g1 = h1 (*) h2 & g2 = h1 ) or ( g1 = h1 (*) h2 & g2 = h1 (*) h2 ) ) by A4, ENUMSET1:def 4;

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

then A41: ( F . g1 = dom f2 & F . g2 = dom f2 ) by A28;
hence A42: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g1 by A40, A27, CAT_6:23
.= (F . g1) (*) (F . g2) by A42, A41, CAT_6:23 ; :: thesis: verum

end;

suppose A43: ( g1 = dom h2 & g2 = cod h2 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A43, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A44: ( g1 = dom h2 & g2 = cod h1 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A44, A5, ZFMISC_1:def 8; :: thesis: verum

end;

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

then cod h2 = g1 by A27, CAT_6:22, CAT_6:27;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A45, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A46: ( g1 = dom h2 & g2 = h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then cod h1 = g1 by A27, CAT_6:22, CAT_6:27;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A46, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A47: ( g1 = dom h2 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then cod (h1 (*) h2) = g1 by A27, CAT_6:22, CAT_6:27;
then cod h1 = g1 by A6, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A47, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A48: ( g1 = cod h2 & g2 = dom h2 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A48, A5, ZFMISC_1:def 8; :: thesis: verum

end;

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

then A50: ( F . g1 = cod f2 & F . g2 = cod f2 ) by A31;
hence A51: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g1 by A49, A27, CAT_6:23
.= (F . g1) (*) (F . g2) by A51, A50, CAT_6:23 ; :: thesis: verum

end;

suppose A52: ( g1 = cod h2 & g2 = cod h1 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A52, A5, ZFMISC_1:def 8; :: thesis: verum

end;

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

then A54: ( F . g1 = cod f2 & F . g2 = f2 ) by A31, A21;
hence F . g1 |> F . g2 by CAT_7:9; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g2 by A53, CAT_7:9
.= (F . g1) (*) (F . g2) by A54, CAT_7:9 ; :: thesis: verum

end;

suppose A55: ( g1 = cod h2 & g2 = h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then cod h1 = g1 by A27, CAT_6:22, CAT_6:27;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A55, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A56: ( g1 = cod h2 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then cod (h1 (*) h2) = g1 by A27, CAT_6:22, CAT_6:27;
then cod h1 = g1 by A6, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A56, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A57: ( g1 = cod h1 & g2 = dom h2 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A57, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A58: ( g1 = cod h1 & g2 = cod h2 ) ; :: 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 A27, CAT_7:7;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A58, A5, ZFMISC_1:def 8; :: thesis: verum

end;

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

then A60: ( F . g1 = cod f1 & F . g2 = cod f1 ) by A34;
hence A61: F . g1 |> F . g2 by CAT_6:23; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g1 by A59, A27, CAT_6:23
.= (F . g1) (*) (F . g2) by A61, A60, CAT_6:23 ; :: thesis: verum

end;

suppose A62: ( g1 = cod h1 & g2 = h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then cod h2 = g1 by A27, CAT_6:22, CAT_6:27;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A62, A5, ZFMISC_1:def 8; :: thesis: verum

end;

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

then A64: ( F . g1 = cod f1 & F . g2 = f1 ) by A34, A24;
hence F . g1 |> F . g2 by CAT_7:9; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g2 by A63, CAT_7:9
.= (F . g1) (*) (F . g2) by A64, CAT_7:9 ; :: thesis: verum

end;

suppose A65: ( g1 = cod h1 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A66: ( F . g1 = cod f1 & F . g2 = f1 (*) f2 ) by A34, A37;
then F . g1 = cod (f1 (*) f2) by A1, CAT_7:4;
hence F . g1 |> F . g2 by A66, CAT_7:9; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
A67: cod (f1 (*) f2) = cod f1 by A1, CAT_7:4;
cod (h1 (*) h2) = cod h1 by A6, CAT_7:4;
hence F . (g1 (*) g2) = F . g2 by A65, CAT_7:9
.= (F . g1) (*) (F . g2) by A66, CAT_7:9, A67 ;
:: thesis: verum

end;

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

then A69: ( F . g1 = f2 & F . g2 = dom f2 ) by A28, A21;
hence F . g1 |> F . g2 by CAT_7:8; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g1 by A68, CAT_7:8
.= (F . g1) (*) (F . g2) by A69, CAT_7:8 ; :: thesis: verum

end;

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

then dom g1 = g2 by A27, CAT_6:22, CAT_6:26;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A70, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A71: ( g1 = h2 & g2 = cod h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then dom g1 = g2 by A27, CAT_6:22, CAT_6:26;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A71, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A72: ( g1 = h2 & g2 = h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then dom g2 = cod g1 by A27, CAT_7:5;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A72, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A73: ( g1 = h2 & g2 = h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod g2 by A27, CAT_7:5;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A73, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A74: ( g1 = h2 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then dom g1 = cod (h1 (*) h2) by A27, CAT_7:5;
then dom g1 = cod h1 by A6, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A74, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A75: ( g1 = h1 & g2 = dom h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

cod h2 = dom h2 by A75, A2, A27, CAT_6:22, CAT_6:26;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A76: ( g1 = h1 & g2 = cod h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A77: ( F . g1 = f1 & F . g2 = cod f2 ) by A31, A24;
then F . g2 is identity by CAT_6:22;
then A78: cod (F . g2) = cod f2 by A77, CAT_7:6;
dom (F . g1) = cod (F . g2) by A78, A77, A1, CAT_7:5;
hence A79: F . g1 |> F . g2 by CAT_7:5; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = F . g1 by A76, CAT_7:8, A2
.= (F . g1) (*) (F . g2) by A79, A77, CAT_6:23 ; :: thesis: verum

end;

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

cod h2 = cod h1 by A80, A2, A27, CAT_6:22, CAT_6:26;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A81: ( g1 = h1 & g2 = h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A82: ( F . g1 = f1 & F . g2 = f2 ) by A21, A24;
hence F . g1 |> F . g2 by A1; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
thus F . (g1 (*) g2) = (F . g1) (*) (F . g2) by A37, A82, A81; :: thesis: verum

end;

suppose A83: ( g1 = h1 & g2 = h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

cod h2 = cod h1 by A83, A2, A27, CAT_7:5;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A84: ( g1 = h1 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then dom g1 = cod (h1 (*) h2) by A27, CAT_7:5;
then dom g1 = cod h1 by A6, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A84, A2, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A85: ( g1 = h1 (*) h2 & g2 = dom h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

then A86: ( F . g1 = f1 (*) f2 & F . g2 = dom f2 ) by A28, A37;
A87: dom (f1 (*) f2) = dom f2 by A1, CAT_7:4;
hence F . g1 |> F . g2 by A86, CAT_7:8; :: thesis: F . (g1 (*) g2) = (F . g1) (*) (F . g2)
dom (h1 (*) h2) = dom h2 by A6, CAT_7:4;
then g1 (*) g2 = h1 (*) h2 by A85, CAT_7:8;
hence F . (g1 (*) g2) = (F . g1) (*) (F . g2) by A85, A87, A86, CAT_7:8; :: thesis: verum

end;

suppose A88: ( g1 = h1 (*) h2 & g2 = cod h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod h2 by A88, A27, CAT_6:22, CAT_6:26;
then dom h2 = cod h2 by A6, A88, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A89: ( g1 = h1 (*) h2 & g2 = cod h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod h1 by A89, A27, CAT_6:22, CAT_6:26;
then dom h2 = cod h1 by A6, A89, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A90: ( g1 = h1 (*) h2 & g2 = h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod h2 by A90, A27, CAT_7:5;
then dom h2 = cod h2 by A6, A90, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A91: ( g1 = h1 (*) h2 & g2 = h1 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod h1 by A91, A27, CAT_7:5;
then dom h2 = cod h1 by A6, A91, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A92: ( g1 = h1 (*) h2 & g2 = h1 (*) h2 ) ; :: thesis: ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) )

dom g1 = cod g2 by A27, CAT_7:5;
then dom g1 = cod h1 by A6, A92, CAT_7:4;
then dom h2 = cod h1 by A6, A92, CAT_7:4;
hence ( F . g1 |> F . g2 & F . (g1 (*) g2) = (F . g1) (*) (F . g2) ) by A5, ZFMISC_1:def 8; :: thesis: verum

end;

end;

end;

then reconsider F = F as covariant Functor of (OrdC 3),C by A20, CAT_6:def 23, CAT_6:def 25;
take F ; :: thesis: for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F . g1 = f1 & F . g2 = f2 )
let g1, g2 be morphism of (OrdC 3); :: thesis: ( g1 |> g2 & not g1 is identity & not g2 is identity implies ( F . g1 = f1 & F . g2 = f2 ) )
assume A93: g1 |> g2 ; :: thesis: ( g1 is identity or g2 is identity or ( F . g1 = f1 & F . g2 = f2 ) )
assume A94: ( not g1 is identity & not g2 is identity ) ; :: thesis: ( F . g1 = f1 & F . g2 = f2 )
A95: ( g1 = dom h2 or g1 = cod h2 or g1 = cod h1 or g1 = h2 or g1 = h1 or g1 = h1 (*) h2 ) by A4, ENUMSET1:def 4;
A96: ( g2 = dom h2 or g2 = cod h2 or g2 = cod h1 or g2 = h2 or g2 = h1 or g2 = h1 (*) h2 ) by A4, ENUMSET1:def 4;
A97: ( g1 = h1 & g2 = h2 )

proof

assume A98: ( g1 <> h1 or g2 <> h2 ) ; :: thesis: contradiction

per cases ( g1 <> h1 or g2 <> h2 ) by A98;

suppose A99: g1 <> h1 ; :: thesis: contradiction

per cases ( ( g1 = h2 & g2 = h2 ) or ( g1 = h2 & g2 = h1 ) or ( g1 = h2 & g2 = h1 (*) h2 ) or ( g1 = h1 (*) h2 & g2 = h2 ) or ( g1 = h1 (*) h2 & g2 = h1 ) or ( g1 = h1 (*) h2 & g2 = h1 (*) h2 ) ) by A99, A95, A96, A94, CAT_6:22;

suppose A100: ( g1 = h2 & g2 = h2 ) ; :: thesis: contradiction

then dom g2 = cod g1 by A93, CAT_7:5;
hence contradiction by A100, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A101: ( g1 = h2 & g2 = h1 ) ; :: thesis: contradiction

dom g1 = cod g2 by A93, CAT_7:5;
hence contradiction by A101, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A102: ( g1 = h2 & g2 = h1 (*) h2 ) ; :: thesis: contradiction

then dom g1 = cod (h1 (*) h2) by A93, CAT_7:5;
then dom g1 = cod h1 by A6, CAT_7:4;
hence contradiction by A102, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A103: ( g1 = h1 (*) h2 & g2 = h2 ) ; :: thesis: contradiction

dom g1 = cod h2 by A103, A93, CAT_7:5;
then dom h2 = cod h2 by A6, A103, CAT_7:4;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A104: ( g1 = h1 (*) h2 & g2 = h1 ) ; :: thesis: contradiction

dom g1 = cod h1 by A104, A93, CAT_7:5;
then dom h2 = cod h1 by A6, A104, CAT_7:4;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A105: ( g1 = h1 (*) h2 & g2 = h1 (*) h2 ) ; :: thesis: contradiction

dom g1 = cod g2 by A93, CAT_7:5;
then dom g1 = cod h1 by A6, A105, CAT_7:4;
then dom h2 = cod h1 by A6, A105, CAT_7:4;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

end;

end;

suppose A106: g2 <> h2 ; :: thesis: contradiction

per cases ( ( g2 = h1 & g1 = h2 ) or ( g2 = h1 & g1 = h1 ) or ( g2 = h1 & g1 = h1 (*) h2 ) or ( g2 = h1 (*) h2 & g1 = h2 ) or ( g2 = h1 (*) h2 & g1 = h1 ) or ( g2 = h1 (*) h2 & g1 = h1 (*) h2 ) ) by A106, A95, A96, A94, CAT_6:22;

suppose A107: ( g2 = h1 & g1 = h2 ) ; :: thesis: contradiction

dom g1 = cod g2 by A93, CAT_7:5;
hence contradiction by A107, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A108: ( g2 = h1 & g1 = h1 ) ; :: thesis: contradiction

cod h2 = cod h1 by A108, A2, A93, CAT_7:5;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A109: ( g2 = h1 & g1 = h1 (*) h2 ) ; :: thesis: contradiction

dom g1 = cod h1 by A109, A93, CAT_7:5;
then dom h2 = cod h1 by A6, A109, CAT_7:4;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A110: ( g2 = h1 (*) h2 & g1 = h2 ) ; :: thesis: contradiction

then dom g1 = cod (h1 (*) h2) by A93, CAT_7:5;
then dom g1 = cod h1 by A6, CAT_7:4;
hence contradiction by A110, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A111: ( g2 = h1 (*) h2 & g1 = h1 ) ; :: thesis: contradiction

then dom g1 = cod (h1 (*) h2) by A93, CAT_7:5;
then dom g1 = cod h1 by A6, CAT_7:4;
hence contradiction by A111, A2, A5, ZFMISC_1:def 8; :: thesis: verum

end;

suppose A112: ( g2 = h1 (*) h2 & g1 = h1 (*) h2 ) ; :: thesis: contradiction

dom g1 = cod g2 by A93, CAT_7:5;
then dom g1 = cod h1 by A6, A112, CAT_7:4;
then dom h2 = cod h1 by A6, A112, CAT_7:4;
hence contradiction by A5, ZFMISC_1:def 8; :: thesis: verum

end;

end;

end;

end;

end;

thus ( F . g1 = f1 & F . g2 = f2 ) by A21, A24, A97; :: thesis: verum

end;

A113: for F1, F2 being covariant Functor of (OrdC 3),C st ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F1 . g1 = f1 & F1 . g2 = f2 ) ) & ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F2 . g1 = f1 & F2 . g2 = f2 ) ) holds
F1 = F2

proof

let F1, F2 be covariant Functor of (OrdC 3),C; :: thesis: ( ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F1 . g1 = f1 & F1 . g2 = f2 ) ) & ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F2 . g1 = f1 & F2 . g2 = f2 ) ) implies F1 = F2 )
assume A114: for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F1 . g1 = f1 & F1 . g2 = f2 ) ; :: thesis: ( ex g1, g2 being morphism of (OrdC 3) st
( g1 |> g2 & not g1 is identity & not g2 is identity & not ( F2 . g1 = f1 & F2 . g2 = f2 ) ) or F1 = F2 )
assume A115: for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( F2 . g1 = f1 & F2 . g2 = f2 ) ; :: thesis: F1 = F2
for x being object st x in the carrier of (OrdC 3) holds
F1 . x = F2 . x

proof

let x be object ; :: thesis: ( x in the carrier of (OrdC 3) implies F1 . x = F2 . x )
assume x in the carrier of (OrdC 3) ; :: thesis: F1 . x = F2 . x
then A116: x in {(dom h2),(cod h2),(cod h1),h2,h1,(h1 (*) h2)} by A4, CAT_6:def 1;
A117: F1 . h1 = f1 by A2, A6, A114
.= F2 . h1 by A2, A6, A115 ;
A118: F1 . h2 = f2 by A2, A6, A114
.= F2 . h2 by A2, A6, A115 ;
A119: ( F1 is multiplicative & F2 is multiplicative ) by CAT_6:def 25;

per cases ( x = dom h2 or x = cod h2 or x = cod h1 or x = h2 or x = h1 or x = h1 (*) h2 ) by A116, ENUMSET1:def 4;

suppose A120: x = dom h2 ; :: thesis: F1 . x = F2 . x

hence F1 . x = dom (F1 . h2) by CAT_6:32
.= F2 . x by A120, A118, CAT_6:32 ;
:: thesis: verum

end;

suppose A121: x = cod h2 ; :: thesis: F1 . x = F2 . x

hence F1 . x = cod (F1 . h2) by CAT_6:32
.= F2 . x by A121, A118, CAT_6:32 ;
:: thesis: verum

end;

suppose A122: x = cod h1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = cod (F1 . h1) by CAT_6:32
.= F2 . x by A122, A117, CAT_6:32 ;
:: thesis: verum

end;

suppose A123: x = h2 ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 . h2 by CAT_6:def 21
.= F2 . x by A123, A118, CAT_6:def 21 ;
:: thesis: verum

end;

suppose A124: x = h1 ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 . h1 by CAT_6:def 21
.= F2 . x by A124, A117, CAT_6:def 21 ;
:: thesis: verum

end;

suppose A125: x = h1 (*) h2 ; :: thesis: F1 . x = F2 . x

hence F1 . x = F1 . (h1 (*) h2) by CAT_6:def 21
.= (F2 . h1) (*) (F2 . h2) by A117, A118, A6, A119, CAT_6:def 23
.= F2 . (h1 (*) h2) by A6, A119, CAT_6:def 23
.= F2 . x by A125, CAT_6:def 21 ;
:: thesis: verum

end;

end;

end;

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

end;

thus ( ex b₁ being covariant Functor of (OrdC 3),C st
for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₁ . g1 = f1 & b₁ . g2 = f2 ) & ( for b₁, b₂ being covariant Functor of (OrdC 3),C st ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₁ . g1 = f1 & b₁ . g2 = f2 ) ) & ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₂ . g1 = f1 & b₂ . g2 = f2 ) ) holds
b₁ = b₂ ) ) by A7, A113; :: thesis: verum