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, 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 #)
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, 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: 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, 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 #)
then A2: the carrier of C1 c= the carrier of C2 by CAT_2:def 4;
A3: the carrier of C2 c= the carrier of C1 by CAT_2:def 4;
then A4: the carrier of C1 = the carrier of C2 by A2, XBOOLE_0:def 10;
A5: the carrier' of C1 c= the carrier' of C2 by A1, CAT_2:7;
A6: the carrier' of C2 c= the carrier' of C1 by CAT_2:7;
then A7: the carrier' of C1 = the carrier' of C2 by A5, XBOOLE_0:def 10;
A8: 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 A9: the Comp of C1 = the Comp of C2 by A8, XBOOLE_0:def 10;

now

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 A5, A6, XBOOLE_0:def 10;
thus the Source of C1 . m1 = dom m1
.= dom m2 by CAT_2:9
.= the Source of C2 . m1 ; :: thesis: verum

end;

then A10: the Source of C1 = the Source of C2 by A4, A7, FUNCT_2:63;

now

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 A5, A6, XBOOLE_0:def 10;
thus the Target of C1 . m1 = cod m1
.= cod m2 by CAT_2:9
.= the Target of C2 . m1 ; :: thesis: verum

end;

then A11: the Target of C1 = the Target of C2 by A4, A7, FUNCT_2:63;

now

let o1 be Object of C1; :: thesis: the Id of C1 . o1 = the Id of C2 . o1
reconsider o2 = o1 as Object of C2 by A2, A3, XBOOLE_0:def 10;
thus the Id of C1 . o1 = id o1
.= id o2 by CAT_2:def 4
.= the Id of C2 . o1 ; :: 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 A4, A7, A9, A10, A11, FUNCT_2:63; :: thesis: verum