let C1 be Category; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: for m1 being Morphism of C1 holds the Source of C1 . m1 = the Source of C2 . m1
let m1 be Morphism of C1; :: thesis: the Source of C1 . m1 = the Source of C2 . m1
reconsider m2 = m1 as Morphism of C2 by A4;
thus the Source of C1 . m1 = dom m1
.= dom m2 by CAT_2:9
.= the Source of C2 . m1 ; :: thesis: verum
end;
then A8: the Source of C1 = the Source of C2 by A3, A5, FUNCT_2:63;
now :: thesis: for m1 being Morphism of C1 holds the Target of C1 . m1 = the Target of C2 . m1
let m1 be Morphism of C1; :: thesis: the Target of C1 . m1 = the Target of C2 . m1
reconsider m2 = m1 as Morphism of C2 by A4;
thus the Target of C1 . m1 = cod m1
.= cod m2 by CAT_2:9
.= the Target of C2 . m1 ; :: thesis: verum
end;
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; :: thesis: verum