thus for C1, C2 being strict AltCatStr st the carrier of C1 = P & ( for i, j being Element of P holds
( the Arrows of C1 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of C1 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) & the carrier of C2 = P & ( for i, j being Element of P holds
( the Arrows of C2 . i,j = MonFuncs i,j & ( for i, j, k being Element of P holds the Comp of C2 . i,j,k = FuncComp (MonFuncs i,j),(MonFuncs j,k) ) ) ) holds
C1 = C2 from ORDERS_3:sch 2(); :: thesis: verum