let C be non empty transitive AltCatStr ; :: thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows 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 transitive SubCatStr of C; :: thesis: ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows 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 ( the carrier of D1 = the carrier of D2 & the Arrows of D1 = the Arrows of D2 ) ; :: thesis: 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 ( D1 is SubCatStr of D2 & D2 is SubCatStr of D1 ) by Th24;
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 Th22; :: thesis: verum