let C be non empty transitive AltCatStr ; for D1, D2 being non empty full SubCatStr of C st the carrier of D1 = the carrier of D2 holds
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
let D1, D2 be non empty full SubCatStr of C; ( the carrier of D1 = the carrier of D2 implies AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #) )
assume A1:
the carrier of D1 = the carrier of D2
; AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
then the Arrows of D1 =
the Arrows of C || the carrier of D2
by Def13
.=
the Arrows of D2
by Def13
;
hence
AltCatStr(# the carrier of D1, the Arrows of D1, the Comp of D1 #) = AltCatStr(# the carrier of D2, the Arrows of D2, the Comp of D2 #)
by A1, Th26; verum