set C = Alter (OrdC 2);

set C1 = Alter (OrdC 2);

set C2 = Alter (OrdC 2);

consider f being morphism of (OrdC 2) such that

not f is identity and

Ob (OrdC 2) = {(dom f),(cod f)} and

A1: Mor (OrdC 2) = {(dom f),(cod f),f} and

A2: dom f, cod f,f are_mutually_distinct by Th39;

reconsider g1 = dom f, g2 = cod f as morphism of (OrdC 2) by A1, ENUMSET1:def 1;

reconsider F1 = MORPHISM g1 as Functor of Alter (OrdC 2), Alter (OrdC 2) by CAT_6:47;

reconsider F2 = MORPHISM g2 as Functor of Alter (OrdC 2), Alter (OrdC 2) by CAT_6:47;

take Alter (OrdC 2) ; :: thesis: ex C1, C2 being Category ex F1 being Functor of C1, Alter (OrdC 2) ex F2 being Functor of C2, Alter (OrdC 2) st

for D being Category

for P1 being Functor of D,C1

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1,C1 ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take Alter (OrdC 2) ; :: thesis: ex C2 being Category ex F1 being Functor of Alter (OrdC 2), Alter (OrdC 2) ex F2 being Functor of C2, Alter (OrdC 2) st

for D being Category

for P1 being Functor of D, Alter (OrdC 2)

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1, Alter (OrdC 2) ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take Alter (OrdC 2) ; :: thesis: ex F1, F2 being Functor of Alter (OrdC 2), Alter (OrdC 2) st

for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take F1 ; :: thesis: ex F2 being Functor of Alter (OrdC 2), Alter (OrdC 2) st

for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take F2 ; :: thesis: for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

assume ex D being Category ex P1, P2 being Functor of D, Alter (OrdC 2) st

( F1 * P1 = F2 * P2 & ( for D1 being Category

for G1, G2 being Functor of D1, Alter (OrdC 2) st F1 * G1 = F2 * G2 holds

ex H being Functor of D1,D st

( P1 * H = G1 & P2 * H = G2 & ( for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2 holds

H = H1 ) ) ) ) ; :: thesis: contradiction

then consider D being Category, P1, P2 being Functor of D, Alter (OrdC 2) such that

A3: ( F1 * P1 = F2 * P2 & ( for D1 being Category

for G1, G2 being Functor of D1, Alter (OrdC 2) st F1 * G1 = F2 * G2 holds

ex H being Functor of D1,D st

( P1 * H = G1 & P2 * H = G2 & ( for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2 holds

H = H1 ) ) ) ) ;

set g = the Morphism of D;

A4: the Morphism of D in the carrier' of D ;

then A5: the Morphism of D in dom P1 by FUNCT_2:def 1;

A6: the Morphism of D in dom P2 by A4, FUNCT_2:def 1;

A7: Alter (OrdC 2) = CatStr(# (Ob (OrdC 2)),(Mor (OrdC 2)),(SourceMap (OrdC 2)),(TargetMap (OrdC 2)),(CompMap (OrdC 2)) #) by CAT_6:def 33;

reconsider f1 = P1 . the Morphism of D as morphism of (OrdC 2) by A7;

reconsider f2 = P2 . the Morphism of D as morphism of (OrdC 2) by A7;

A8: (F1 * P1) . the Morphism of D = F1 . (P1 . the Morphism of D) by A5, FUNCT_1:13

.= (MORPHISM g1) . f1 by CAT_6:def 21

.= g1 by Th40, CAT_6:22 ;

(F2 * P2) . the Morphism of D = F2 . (P2 . the Morphism of D) by A6, FUNCT_1:13

.= (MORPHISM g2) . f2 by CAT_6:def 21

.= g2 by Th40, CAT_6:22 ;

hence contradiction by A8, A3, A2, ZFMISC_1:def 5; :: thesis: verum

set C1 = Alter (OrdC 2);

set C2 = Alter (OrdC 2);

consider f being morphism of (OrdC 2) such that

not f is identity and

Ob (OrdC 2) = {(dom f),(cod f)} and

A1: Mor (OrdC 2) = {(dom f),(cod f),f} and

A2: dom f, cod f,f are_mutually_distinct by Th39;

reconsider g1 = dom f, g2 = cod f as morphism of (OrdC 2) by A1, ENUMSET1:def 1;

reconsider F1 = MORPHISM g1 as Functor of Alter (OrdC 2), Alter (OrdC 2) by CAT_6:47;

reconsider F2 = MORPHISM g2 as Functor of Alter (OrdC 2), Alter (OrdC 2) by CAT_6:47;

take Alter (OrdC 2) ; :: thesis: ex C1, C2 being Category ex F1 being Functor of C1, Alter (OrdC 2) ex F2 being Functor of C2, Alter (OrdC 2) st

for D being Category

for P1 being Functor of D,C1

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1,C1 ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take Alter (OrdC 2) ; :: thesis: ex C2 being Category ex F1 being Functor of Alter (OrdC 2), Alter (OrdC 2) ex F2 being Functor of C2, Alter (OrdC 2) st

for D being Category

for P1 being Functor of D, Alter (OrdC 2)

for P2 being Functor of D,C2 holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1 being Functor of D1, Alter (OrdC 2) ex G2 being Functor of D1,C2 st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take Alter (OrdC 2) ; :: thesis: ex F1, F2 being Functor of Alter (OrdC 2), Alter (OrdC 2) st

for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take F1 ; :: thesis: ex F2 being Functor of Alter (OrdC 2), Alter (OrdC 2) st

for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

take F2 ; :: thesis: for D being Category

for P1, P2 being Functor of D, Alter (OrdC 2) holds

( not F1 * P1 = F2 * P2 or ex D1 being Category ex G1, G2 being Functor of D1, Alter (OrdC 2) st

( F1 * G1 = F2 * G2 & ( for H being Functor of D1,D holds

( not P1 * H = G1 or not P2 * H = G2 or ex H1 being Functor of D1,D st

( P1 * H1 = G1 & P2 * H1 = G2 & not H = H1 ) ) ) ) )

assume ex D being Category ex P1, P2 being Functor of D, Alter (OrdC 2) st

( F1 * P1 = F2 * P2 & ( for D1 being Category

for G1, G2 being Functor of D1, Alter (OrdC 2) st F1 * G1 = F2 * G2 holds

ex H being Functor of D1,D st

( P1 * H = G1 & P2 * H = G2 & ( for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2 holds

H = H1 ) ) ) ) ; :: thesis: contradiction

then consider D being Category, P1, P2 being Functor of D, Alter (OrdC 2) such that

A3: ( F1 * P1 = F2 * P2 & ( for D1 being Category

for G1, G2 being Functor of D1, Alter (OrdC 2) st F1 * G1 = F2 * G2 holds

ex H being Functor of D1,D st

( P1 * H = G1 & P2 * H = G2 & ( for H1 being Functor of D1,D st P1 * H1 = G1 & P2 * H1 = G2 holds

H = H1 ) ) ) ) ;

set g = the Morphism of D;

A4: the Morphism of D in the carrier' of D ;

then A5: the Morphism of D in dom P1 by FUNCT_2:def 1;

A6: the Morphism of D in dom P2 by A4, FUNCT_2:def 1;

A7: Alter (OrdC 2) = CatStr(# (Ob (OrdC 2)),(Mor (OrdC 2)),(SourceMap (OrdC 2)),(TargetMap (OrdC 2)),(CompMap (OrdC 2)) #) by CAT_6:def 33;

reconsider f1 = P1 . the Morphism of D as morphism of (OrdC 2) by A7;

reconsider f2 = P2 . the Morphism of D as morphism of (OrdC 2) by A7;

A8: (F1 * P1) . the Morphism of D = F1 . (P1 . the Morphism of D) by A5, FUNCT_1:13

.= (MORPHISM g1) . f1 by CAT_6:def 21

.= g1 by Th40, CAT_6:22 ;

(F2 * P2) . the Morphism of D = F2 . (P2 . the Morphism of D) by A6, FUNCT_1:13

.= (MORPHISM g2) . f2 by CAT_6:def 21

.= g2 by Th40, CAT_6:22 ;

hence contradiction by A8, A3, A2, ZFMISC_1:def 5; :: thesis: verum