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