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