A1:
for i, j, k being Element of P
for f, g being Function st f in MonFuncs (i,j) & g in MonFuncs (j,k) holds
g * f in MonFuncs (i,k)
by Th6;
thus
ex C being strict AltCatStr st
( the carrier of C = P & ( for i, j being Element of P holds
( the Arrows of C . (i,j) = MonFuncs (i,j) & ( for i, j, k being Element of P holds the Comp of C . (i,j,k) = FuncComp ((MonFuncs (i,j)),(MonFuncs (j,k))) ) ) ) )
from ORDERS_3:sch 1(A1); verum