let C1 be Category; for C2 being Subcategory of C1 st C1 is Subcategory of C2 holds
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 #)
let C2 be Subcategory of C1; ( C1 is Subcategory 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:
C1 is Subcategory 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 #)
then A2:
the carrier of C1 c= the carrier of C2
by CAT_2:def 4;
the carrier of C2 c= the carrier of C1
by CAT_2:def 4;
then A3:
the carrier of C1 = the carrier of C2
by A2;
A4:
the carrier' of C1 c= the carrier' of C2
by A1, CAT_2:7;
the carrier' of C2 c= the carrier' of C1
by CAT_2:7;
then A5:
the carrier' of C1 = the carrier' of C2
by A4;
A6:
the Comp of C1 c= the Comp of C2
by A1, CAT_2:def 4;
the Comp of C2 c= the Comp of C1
by CAT_2:def 4;
then A7:
the Comp of C1 = the Comp of C2
by A6;
then A8:
the Source of C1 = the Source of C2
by A3, A5, FUNCT_2:63;
then
the Target of C1 = the Target of C2
by A3, A5, FUNCT_2:63;
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 A3, A5, A7, A8; verum