let C be non empty transitive AltCatStr ; :: thesis: 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; :: thesis: ( 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 ; :: 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 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, Th27; :: thesis: verum