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 #)
A2: the carrier of C1 = the carrier of C2

proof

thus the carrier of C1 c= the carrier of C2 by A1, CAT_2:def 4; :: according to XBOOLE_0:def 10 :: thesis: the carrier of C2 c= the carrier of C1
thus the carrier of C2 c= the carrier of C1 by CAT_2:def 4; :: thesis: verum

end;

A3: the carrier' of C1 = the carrier' of C2

proof

thus the carrier' of C1 c= the carrier' of C2 by A1, CAT_2:13; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of C2 c= the carrier' of C1
thus the carrier' of C2 c= the carrier' of C1 by CAT_2:13; :: thesis: verum

end;

A4: the Comp of C1 = the Comp of C2

proof

thus the Comp of C1 c= the Comp of C2 by A1, CAT_2:def 4; :: according to XBOOLE_0:def 10 :: thesis: the Comp of C2 c= the Comp of C1
thus the Comp of C2 c= the Comp of C1 by CAT_2:def 4; :: thesis: verum

end;

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 A3;
thus the Source of C1 . m1 = dom m1
.= dom m2 by CAT_2:15
.= the Source of C2 . m1 ; :: thesis: verum

end;

then A5: the Source of C1 = the Source of C2 by A2, A3, FUNCT_2:113;

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 A3;
thus the Target of C1 . m1 = cod m1
.= cod m2 by CAT_2:15
.= the Target of C2 . m1 ; :: thesis: verum

end;

then A6: the Target of C1 = the Target of C2 by A2, A3, FUNCT_2:113;

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;
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 A2, A3, A4, A5, A6, FUNCT_2:113; :: thesis: verum