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 A1: ( the carrier of A = the carrier of C & the carrier' of A = the carrier' of C ) ; :: thesis: A = C
A2: ( dom the Source of C = the carrier' of C & dom the Target of C = the carrier' of C & dom the Id of C = the carrier of C ) by FUNCT_2:def 1;

now

thus the Source of A = the Source of C | the carrier' of A by Th8
.= the Source of C by A1, A2, RELAT_1:97 ; :: thesis: ( the Target of A = the Target of C & the Comp of A = the Comp of C & the Id of A = the Id of C )
thus the Target of A = the Target of C | the carrier' of A by Th8
.= the Target of C by A1, A2, RELAT_1:97 ; :: thesis: ( the Comp of A = the Comp of C & the Id of A = the Id of C )
A3: dom the Comp of C c= [:the carrier' of C,the carrier' of C:] by RELAT_1:def 18;
thus the Comp of A = the Comp of C || the carrier' of A by Th8
.= the Comp of C by A1, A3, RELAT_1:97 ; :: thesis: the Id of A = the Id of C
thus the Id of A = the Id of C | the carrier of A by Th8
.= the Id of C by A1, A2, RELAT_1:97 ; :: thesis: verum

end;

hence A = C by A1; :: thesis: verum