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