consider C being strict preorder category such that

A1: Ob C = 2 and

for o1, o2 being Object of C st o1 in o2 holds

Hom (o1,o2) = {[o1,o2]} and

A2: RelOb C = RelIncl 2 and

A3: Mor C = 2 \/ { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } by Th37;

A4: C is 2 -ordered by A2, WELLORD1:38;

then A5: C ~= OrdC 2 by Th38;

consider F being Functor of C,(OrdC 2), G being Functor of (OrdC 2),C such that

A6: ( F is covariant & G is covariant ) and

A7: ( G (*) F = id C & F (*) G = id (OrdC 2) ) by A4, Th38, CAT_6:def 28;

( 0 in 1 & 0 is Element of 2 & 1 is Element of 2 ) by CARD_1:49, CARD_1:50, TARSKI:def 1, TARSKI:def 2;

then A8: [0,1] in { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } ;

then A9: [0,1] in Mor C by A3, XBOOLE_0:def 3;

reconsider g = [0,1] as morphism of C by A8, A3, XBOOLE_0:def 3;

A10: not C is empty by A1;

A11: not g is identity

take F . g ; :: thesis: ( not F . g is identity & Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )

thus A12: not F . g is identity :: thesis: ( Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )

then consider x, y being object such that

A15: ( x <> y & Ob (OrdC 2) = {x,y} ) by CARD_2:60;

A16: ( dom (F . g) = x or dom (F . g) = y ) by A15, TARSKI:def 2;

A17: dom (F . g) <> cod (F . g)

for x being object holds

( x in Mor (OrdC 2) iff x in {(dom (F . g)),(cod (F . g)),(F . g)} )

( dom (F . g) <> cod (F . g) & dom (F . g) <> F . g & cod (F . g) <> F . g ) by A12, A17, CAT_6:22;

hence dom (F . g), cod (F . g),F . g are_mutually_distinct by ZFMISC_1:def 5; :: thesis: verum

A1: Ob C = 2 and

for o1, o2 being Object of C st o1 in o2 holds

Hom (o1,o2) = {[o1,o2]} and

A2: RelOb C = RelIncl 2 and

A3: Mor C = 2 \/ { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } by Th37;

A4: C is 2 -ordered by A2, WELLORD1:38;

then A5: C ~= OrdC 2 by Th38;

consider F being Functor of C,(OrdC 2), G being Functor of (OrdC 2),C such that

A6: ( F is covariant & G is covariant ) and

A7: ( G (*) F = id C & F (*) G = id (OrdC 2) ) by A4, Th38, CAT_6:def 28;

( 0 in 1 & 0 is Element of 2 & 1 is Element of 2 ) by CARD_1:49, CARD_1:50, TARSKI:def 1, TARSKI:def 2;

then A8: [0,1] in { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } ;

then A9: [0,1] in Mor C by A3, XBOOLE_0:def 3;

reconsider g = [0,1] as morphism of C by A8, A3, XBOOLE_0:def 3;

A10: not C is empty by A1;

A11: not g is identity

proof

set f = F . g;
assume
g is identity
; :: thesis: contradiction

then g is Object of C by A10, CAT_6:22;

hence contradiction by A1; :: thesis: verum

end;then g is Object of C by A10, CAT_6:22;

hence contradiction by A1; :: thesis: verum

take F . g ; :: thesis: ( not F . g is identity & Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )

thus A12: not F . g is identity :: thesis: ( Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))} & Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )

proof

card (Ob (OrdC 2)) = card 2
by A1, A5, Th14;
assume A13:
F . g is identity
; :: thesis: contradiction

[0,1] in the carrier of C by A9, CAT_6:def 1;

then (id the carrier of C) . [0,1] = [0,1] by FUNCT_1:18;

then A14: (id C) . [0,1] = g by STRUCT_0:def 4;

G . (F . g) is identity by A13, CAT_6:def 22, A6, CAT_6:def 25;

then (G (*) F) . g is identity by A6, A10, CAT_6:34;

hence contradiction by A11, A7, A10, A14, CAT_6:def 21; :: thesis: verum

end;[0,1] in the carrier of C by A9, CAT_6:def 1;

then (id the carrier of C) . [0,1] = [0,1] by FUNCT_1:18;

then A14: (id C) . [0,1] = g by STRUCT_0:def 4;

G . (F . g) is identity by A13, CAT_6:def 22, A6, CAT_6:def 25;

then (G (*) F) . g is identity by A6, A10, CAT_6:34;

hence contradiction by A11, A7, A10, A14, CAT_6:def 21; :: thesis: verum

then consider x, y being object such that

A15: ( x <> y & Ob (OrdC 2) = {x,y} ) by CARD_2:60;

A16: ( dom (F . g) = x or dom (F . g) = y ) by A15, TARSKI:def 2;

A17: dom (F . g) <> cod (F . g)

proof

hence A19:
Ob (OrdC 2) = {(dom (F . g)),(cod (F . g))}
by A15, A16, TARSKI:def 2; :: thesis: ( Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)} & dom (F . g), cod (F . g),F . g are_mutually_distinct )
assume
dom (F . g) = cod (F . g)
; :: thesis: contradiction

then A18: F . g in Hom ((dom (F . g)),(dom (F . g))) ;

id- (dom (F . g)) in Hom ((dom (F . g)),(dom (F . g))) by Def3;

hence contradiction by A12, A18, Def12; :: thesis: verum

end;then A18: F . g in Hom ((dom (F . g)),(dom (F . g))) ;

id- (dom (F . g)) in Hom ((dom (F . g)),(dom (F . g))) by Def3;

hence contradiction by A12, A18, Def12; :: thesis: verum

for x being object holds

( x in Mor (OrdC 2) iff x in {(dom (F . g)),(cod (F . g)),(F . g)} )

proof

hence
Mor (OrdC 2) = {(dom (F . g)),(cod (F . g)),(F . g)}
by TARSKI:2; :: thesis: dom (F . g), cod (F . g),F . g are_mutually_distinct
let x be object ; :: thesis: ( x in Mor (OrdC 2) iff x in {(dom (F . g)),(cod (F . g)),(F . g)} )

then A27: x in {(dom (F . g)),(cod (F . g))} \/ {(F . g)} by ENUMSET1:3;

end;hereby :: thesis: ( x in {(dom (F . g)),(cod (F . g)),(F . g)} implies x in Mor (OrdC 2) )

assume
x in {(dom (F . g)),(cod (F . g)),(F . g)}
; :: thesis: x in Mor (OrdC 2)assume A20:
x in Mor (OrdC 2)
; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}

then A21: x in the carrier of (OrdC 2) by CAT_6:def 1;

reconsider f1 = x as morphism of (OrdC 2) by A20;

end;then A21: x in the carrier of (OrdC 2) by CAT_6:def 1;

reconsider f1 = x as morphism of (OrdC 2) by A20;

per cases
( f1 is identity or not f1 is identity )
;

end;

suppose
f1 is identity
; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}

then
f1 is Object of (OrdC 2)
by CAT_6:22;

then ( x = dom (F . g) or x = cod (F . g) ) by A19, TARSKI:def 2;

hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by ENUMSET1:def 1; :: thesis: verum

end;then ( x = dom (F . g) or x = cod (F . g) ) by A19, TARSKI:def 2;

hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by ENUMSET1:def 1; :: thesis: verum

suppose A22:
not f1 is identity
; :: thesis: x in {(dom (F . g)),(cod (F . g)),(F . g)}

A23:
(id the carrier of (OrdC 2)) . x = x
by A21, FUNCT_1:18;

A24: F . (G . f1) = (F (*) G) . f1 by A6, CAT_6:34

.= (id the carrier of (OrdC 2)) . f1 by A7, STRUCT_0:def 4

.= f1 by A23, CAT_6:def 21 ;

not G . f1 is identity by A24, A22, CAT_6:def 22, A6, CAT_6:def 25;

then not G . f1 in 2 by A1, A10, CAT_6:22;

then G . f1 in { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } by A3, XBOOLE_0:def 3;

then consider o1, o2 being Element of 2 such that

A25: ( G . f1 = [o1,o2] & o1 in o2 ) ;

A26: ( o1 = 0 or o1 = 1 ) by CARD_1:50, TARSKI:def 2;

( o2 = 0 or o2 = 1 ) by CARD_1:50, TARSKI:def 2;

hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by A25, A26, A24, ENUMSET1:def 1, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;A24: F . (G . f1) = (F (*) G) . f1 by A6, CAT_6:34

.= (id the carrier of (OrdC 2)) . f1 by A7, STRUCT_0:def 4

.= f1 by A23, CAT_6:def 21 ;

not G . f1 is identity by A24, A22, CAT_6:def 22, A6, CAT_6:def 25;

then not G . f1 in 2 by A1, A10, CAT_6:22;

then G . f1 in { [o1,o2] where o1, o2 is Element of 2 : o1 in o2 } by A3, XBOOLE_0:def 3;

then consider o1, o2 being Element of 2 such that

A25: ( G . f1 = [o1,o2] & o1 in o2 ) ;

A26: ( o1 = 0 or o1 = 1 ) by CARD_1:50, TARSKI:def 2;

( o2 = 0 or o2 = 1 ) by CARD_1:50, TARSKI:def 2;

hence x in {(dom (F . g)),(cod (F . g)),(F . g)} by A25, A26, A24, ENUMSET1:def 1, CARD_1:49, TARSKI:def 1; :: thesis: verum

then A27: x in {(dom (F . g)),(cod (F . g))} \/ {(F . g)} by ENUMSET1:3;

( dom (F . g) <> cod (F . g) & dom (F . g) <> F . g & cod (F . g) <> F . g ) by A12, A17, CAT_6:22;

hence dom (F . g), cod (F . g),F . g are_mutually_distinct by ZFMISC_1:def 5; :: thesis: verum