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 #)
A2: dom the Arrows of C = [: the carrier of C, the carrier of C:] by PARTFUN1:def 2;
the Arrows of D = the Arrows of C || the carrier of D by Def13
.= the Arrows of C by A1, A2, RELAT_1:69 ;
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, Th26; :: thesis: verum