let C1, C2 be Categorial full Category; ( the carrier of C1 = the carrier of C2 implies CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) )
assume A1:
the carrier of C1 = the carrier of C2
; CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)
reconsider A = the carrier of C1 as non empty categorial set by Def6;
set B = { (m `2) where m is Morphism of C1 : verum } ;
set m = the Morphism of C1;
the Morphism of C1 `2 in { (m `2) where m is Morphism of C1 : verum }
;
then reconsider B = { (m `2) where m is Morphism of C1 : verum } as non empty set ;
reconsider D1 = CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #), D2 = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) as strict Category by Th1;
A2:
D1 is Categorial
by Th10;
A3:
D2 is Categorial
by Th10;
A4:
now for a, b being Element of A
for F being Functor of a,b holds
( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B )let a,
b be
Element of
A;
for F being Functor of a,b holds
( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B )let F be
Functor of
a,
b;
( [[a,b],F] is Morphism of CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) iff F in B )reconsider m =
[[a,b],F] as
Morphism of
C1 by Def8;
m `2 = F
;
hence
(
[[a,b],F] is
Morphism of
CatStr(# the
carrier of
C1, the
carrier' of
C1, the
Source of
C1, the
Target of
C1, the
Comp of
C1 #) iff
F in B )
;
verum end;
now for a, b being Element of A
for F being Functor of a,b holds
( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B )let a,
b be
Element of
A;
for F being Functor of a,b holds
( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B )let F be
Functor of
a,
b;
( [[a,b],F] is Morphism of CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #) iff F in B )reconsider a9 =
a,
b9 =
b as
Object of
C2 by A1;
A5:
cat a9 = a
by Th16;
cat b9 = b
by Th16;
then reconsider m2 =
[[a,b],F] as
Morphism of
C2 by A5, Def8;
reconsider m =
[[a,b],F] as
Morphism of
C1 by Def8;
A6:
m `2 = F
;
m2 = m2
;
hence
(
[[a,b],F] is
Morphism of
CatStr(# the
carrier of
C2, the
carrier' of
C2, the
Source of
C2, the
Target of
C2, the
Comp of
C2 #) iff
F in B )
by A6;
verum end;
hence
CatStr(# the carrier of C1, the carrier' of C1, the Source of C1, the Target of C1, the Comp of C1 #) = CatStr(# the carrier of C2, the carrier' of C2, the Source of C2, the Target of C2, the Comp of C2 #)
by A1, A2, A3, A4, Th18; verum