let It1, It2 be strict discrete Subcategory of C; :: thesis: ( the carrier of It1 = the carrier of C & the carrier' of It1 = { (id a) where a is Object of C : verum } & the carrier of It2 = the carrier of C & the carrier' of It2 = { (id a) where a is Object of C : verum } implies It1 = It2 )
assume that
A22: ( the carrier of It1 = the carrier of C & the carrier' of It1 = { (id a) where a is Object of C : verum } ) and
A23: ( the carrier of It2 = the carrier of C & the carrier' of It2 = { (id a) where a is Object of C : verum } ) ; :: thesis: It1 = It2
set M = the carrier' of It1;
A24: ( the Source of It1 = the Source of C | the carrier' of It1 & the Source of It2 = the Source of C | the carrier' of It1 ) by A22, A23, Th8;
A25: ( the Target of It1 = the Target of C | the carrier' of It1 & the Target of It2 = the Target of C | the carrier' of It1 ) by A22, A23, Th8;
A26: ( the Comp of It1 = the Comp of C || the carrier' of It1 & the Comp of It2 = the Comp of C || the carrier' of It1 ) by A22, A23, Th8;
( the Id of It1 = the Id of C | the carrier of It1 & the Id of It2 = the Id of C | the carrier of It2 ) by Th8;
hence It1 = It2 by A22, A23, A24, A25, A26; :: thesis: verum