let C be strict Category; :: thesis: for A being strict Subcategory of C st the carrier of A = the carrier of C & the carrier' of A = the carrier' of C holds
A = C
let A be strict Subcategory of C; :: thesis: ( the carrier of A = the carrier of C & the carrier' of A = the carrier' of C implies A = C )
assume that
A1: the carrier of A = the carrier of C and
A2: the carrier' of A = the carrier' of C ; :: thesis: A = C
A3: dom the Target of C = the carrier' of C by FUNCT_2:def 1;
A4: dom the Id of C = the carrier of C by FUNCT_2:def 1;
A5: the Id of A = the Id of C | the carrier of A by Th8
.= the Id of C by A1, A4, RELAT_1:68 ;
A6: dom the Source of C = the carrier' of C by FUNCT_2:def 1;
A7: the Target of A = the Target of C | the carrier' of A by Th8
.= the Target of C by A2, A3, RELAT_1:68 ;
A8: dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def 18;
A9: the Comp of A = the Comp of C || the carrier' of A by Th8
.= the Comp of C by A2, A8, RELAT_1:68 ;
the Source of A = the Source of C | the carrier' of A by Th8
.= the Source of C by A2, A6, RELAT_1:68 ;
hence A = C by A1, A2, A7, A9, A5; :: thesis: verum