consider C being strict preorder category such that
A1: Ob C = 1 and
for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} and
A2: RelOb C = RelIncl 1 and
A3: Mor C = 1 \/ { [o1,o2] where o1, o2 is Element of 1 : o1 in o2 } by CAT_7:37;
A4: C is 1 -ordered by A2, WELLORD1:38, CAT_7:def 14;
then A5: C ~= OrdC 1 by CAT_7:38;
consider F being Functor of C,(OrdC 1), G being Functor of (OrdC 1),C such that
A6: ( F is covariant & G is covariant ) and
A7: ( G (*) F = id C & F (*) G = id (OrdC 1) ) by A4, CAT_7:38, CAT_6:def 28;
A8: 0 in Ob C by A1, CARD_1:49, TARSKI:def 1;
then reconsider g = 0 as morphism of C ;
A9: not C is empty by A1;
then A10: g is identity by A8, CAT_6:22;
set f = F . g;
take F . g ; :: thesis: ( F . g is identity & Ob (OrdC 1) = {(F . g)} & Mor (OrdC 1) = {(F . g)} )
thus A11: F . g is identity by A6, A10, CAT_6:def 22, CAT_6:def 25; :: thesis: ( Ob (OrdC 1) = {(F . g)} & Mor (OrdC 1) = {(F . g)} )
card (Ob (OrdC 1)) = card 1 by A1, A5, CAT_7:14;
then consider x being object such that
A12: Ob (OrdC 1) = {x} by CARD_2:42;
F . g is Object of (OrdC 1) by A11, CAT_6:22;
hence A13: Ob (OrdC 1) = {(F . g)} by A12, TARSKI:def 1; :: thesis: Mor (OrdC 1) = {(F . g)}
for x being object holds
( x in Mor (OrdC 1) iff x in {(F . g)} )

proof

let x be object ; :: thesis: ( x in Mor (OrdC 1) iff x in {(F . g)} )

hereby :: thesis: ( x in {(F . g)} implies x in Mor (OrdC 1) )

assume A14: x in Mor (OrdC 1) ; :: thesis: x in {(F . g)}
then A15: x in the carrier of (OrdC 1) by CAT_6:def 1;
reconsider f1 = x as morphism of (OrdC 1) by A14;

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

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

then f1 is Object of (OrdC 1) by CAT_6:22;
hence x in {(F . g)} by A13; :: thesis: verum

end;

suppose A16: not f1 is identity ; :: thesis: x in {(F . g)}

A17: (id the carrier of (OrdC 1)) . x = x by A15, FUNCT_1:18;
A18: F . (G . f1) = (F (*) G) . f1 by A6, CAT_6:34
.= (id the carrier of (OrdC 1)) . f1 by A7, STRUCT_0:def 4
.= f1 by A17, CAT_6:def 21 ;
not G . f1 is identity by A18, A16, CAT_6:def 22, A6, CAT_6:def 25;
then not G . f1 in 1 by A1, A9, CAT_6:22;
then G . f1 in { [o1,o2] where o1, o2 is Element of 1 : o1 in o2 } by A3, XBOOLE_0:def 3;
then consider o1, o2 being Element of 1 such that
A19: ( G . f1 = [o1,o2] & o1 in o2 ) ;
A20: o1 = 0 by CARD_1:49, TARSKI:def 1;
o2 = 0 by CARD_1:49, TARSKI:def 1;
hence x in {(F . g)} by A19, A20; :: thesis: verum

end;

end;

end;

assume x in {(F . g)} ; :: thesis: x in Mor (OrdC 1)
hence x in Mor (OrdC 1) by A13; :: thesis: verum

end;

hence Mor (OrdC 1) = {(F . g)} by TARSKI:2; :: thesis: verum