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: the Target of A = the Target of C | the carrier' of A by Th4

.= the Target of C by A2 ;

A4: the Comp of A = the Comp of C || the carrier' of A by Th4

.= the Comp of C by A2 ;

the Source of A = the Source of C | the carrier' of A by Th4

.= the Source of C by A2 ;

hence A = C by A1, A3, A4; :: thesis: verum

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: the Target of A = the Target of C | the carrier' of A by Th4

.= the Target of C by A2 ;

A4: the Comp of A = the Comp of C || the carrier' of A by Th4

.= the Comp of C by A2 ;

the Source of A = the Source of C | the carrier' of A by Th4

.= the Source of C by A2 ;

hence A = C by A1, A3, A4; :: thesis: verum