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