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); :: thesis: verum