let It1, It2 be strict discrete Subcategory of C; ( 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
A23:
the carrier of It1 = the carrier of C
and
A24:
the carrier' of It1 = { (id a) where a is Object of C : verum }
and
A25:
the carrier of It2 = the carrier of C
and
A26:
the carrier' of It2 = { (id a) where a is Object of C : verum }
; It1 = It2
set M = the carrier' of It1;
A27:
the Target of It2 = the Target of C | the carrier' of It1
by A24, A26, Th8;
A28:
the Comp of It2 = the Comp of C || the carrier' of It1
by A24, A26, Th8;
A29:
the Source of It1 = the Source of C | the carrier' of It1
by Th8;
A30:
the Id of It1 = the Id of C | the carrier of It1
by Th8;
A31:
the Comp of It1 = the Comp of C || the carrier' of It1
by Th8;
A32:
the Target of It1 = the Target of C | the carrier' of It1
by Th8;
the Source of It2 = the Source of C | the carrier' of It1
by A24, A26, Th8;
hence
It1 = It2
by A23, A24, A25, A26, A29, A32, A27, A31, A28, A30, Th8; verum