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 that
A1: the carrier of D1 = the carrier of D2 and
A2: 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 #)
A3: D1 is SubCatStr of D2 by A1, A2, Th25;
D2 is SubCatStr of D1 by A1, A2, Th25;
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 A3, Th23; :: thesis: verum