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
A20:
the carrier of It1 = the carrier of C
and
A21:
the carrier' of It1 = { (id a) where a is Object of C : verum }
and
A22:
the carrier of It2 = the carrier of C
and
A23:
the carrier' of It2 = { (id a) where a is Object of C : verum }
; It1 = It2
set M = the carrier' of It1;
A24:
the Target of It2 = the Target of C | the carrier' of It1
by A21, A23, Th8;
A25:
the Comp of It2 = the Comp of C || the carrier' of It1
by A21, A23, Th8;
A26:
the Source of It1 = the Source of C | the carrier' of It1
by Th8;
A27:
the Comp of It1 = the Comp of C || the carrier' of It1
by Th8;
the Target of It1 = the Target of C | the carrier' of It1
by Th8;
hence
It1 = It2
by A20, A21, A22, A23, A26, A24, A27, A25, Th8; verum