let C1, C2 be Categorial full Category; :: thesis: ( 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,the Id of C1 #) = CatStr(# the carrier of C2,the carrier' of C2,the Source of C2,the Target of C2,the Comp of C2,the Id of C2 #) )
assume A1:
the carrier of C1 = the carrier of C2
; :: thesis: CatStr(# the carrier of C1,the carrier' of C1,the Source of C1,the Target of C1,the Comp of C1,the Id of C1 #) = CatStr(# the carrier of C2,the carrier' of C2,the Source of C2,the Target of C2,the Comp of C2,the Id 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 } ;
consider m being Morphism of C1;
m `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,the Id of C1 #), D2 = CatStr(# the carrier of C2,the carrier' of C2,the Source of C2,the Target of C2,the Comp of C2,the Id of C2 #) as strict Category by Th1;
A2:
( D1 is Categorial & D2 is Categorial )
by Th10;
A3:
now let a,
b be
Element of
A;
:: thesis: 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,the Id of C1 #) iff F in B )let F be
Functor of
a,
b;
:: thesis: ( [[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,the Id of C1 #) iff F in B )reconsider m =
[[a,b],F] as
Morphism of
C1 by Def8;
m `2 = F
by MCART_1:7;
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,the
Id of
C1 #) iff
F in B )
;
:: thesis: verum end;
now let a,
b be
Element of
A;
:: thesis: 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,the Id of C2 #) iff F in B )let F be
Functor of
a,
b;
:: thesis: ( [[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,the Id of C2 #) iff F in B )reconsider a' =
a,
b' =
b as
Object of
C2 by A1;
(
cat a' = a &
cat b' = b )
by Th16;
then reconsider m2 =
[[a,b],F] as
Morphism of
C2 by Def8;
reconsider m =
[[a,b],F] as
Morphism of
C1 by Def8;
(
m `2 = F &
m2 = m2 )
by MCART_1:7;
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,the
Id of
C2 #) iff
F in B )
;
:: thesis: verum end;
hence
CatStr(# the carrier of C1,the carrier' of C1,the Source of C1,the Target of C1,the Comp of C1,the Id of C1 #) = CatStr(# the carrier of C2,the carrier' of C2,the Source of C2,the Target of C2,the Comp of C2,the Id of C2 #)
by A1, A2, A3, Th18; :: thesis: verum