let C be non empty transitive AltCatStr ; :: thesis: for D being full SubCatStr of C st the carrier of D = the carrier of C holds

AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

let D be full SubCatStr of C; :: thesis: ( the carrier of D = the carrier of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )

assume A1: the carrier of D = the carrier of C ; :: thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

the Arrows of D = the Arrows of C || the carrier of D by Def13

.= the Arrows of C by A1 ;

hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by A1, Th25; :: thesis: verum

AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

let D be full SubCatStr of C; :: thesis: ( the carrier of D = the carrier of C implies AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) )

assume A1: the carrier of D = the carrier of C ; :: thesis: AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #)

the Arrows of D = the Arrows of C || the carrier of D by Def13

.= the Arrows of C by A1 ;

hence AltCatStr(# the carrier of D, the Arrows of D, the Comp of D #) = AltCatStr(# the carrier of C, the Arrows of C, the Comp of C #) by A1, Th25; :: thesis: verum