set A = POSAltCat P;
set G = the Arrows of (POSAltCat P);
set C = the Comp of (POSAltCat P);
thus the Comp of (POSAltCat P) is associative :: according to ALTCAT_1:def 17 :: thesis: POSAltCat P is with_units

proof

let i, j, k, l be Element of (POSAltCat P); :: according to ALTCAT_1:def 7 :: thesis: for b₁, b₂, b₃ being set holds
( not b₁ in the Arrows of (POSAltCat P) . i,j or not b₂ in the Arrows of (POSAltCat P) . j,k or not b₃ in the Arrows of (POSAltCat P) . k,l or (the Comp of (POSAltCat P) . i,k,l) . b₃,((the Comp of (POSAltCat P) . i,j,k) . b₂,b₁) = (the Comp of (POSAltCat P) . i,j,l) . ((the Comp of (POSAltCat P) . j,k,l) . b₃,b₂),b₁ )
let f, g, h be set ; :: thesis: ( not f in the Arrows of (POSAltCat P) . i,j or not g in the Arrows of (POSAltCat P) . j,k or not h in the Arrows of (POSAltCat P) . k,l or (the Comp of (POSAltCat P) . i,k,l) . h,((the Comp of (POSAltCat P) . i,j,k) . g,f) = (the Comp of (POSAltCat P) . i,j,l) . ((the Comp of (POSAltCat P) . j,k,l) . h,g),f )
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of P by Def9;
assume that
A1: f in the Arrows of (POSAltCat P) . i,j and
A2: g in the Arrows of (POSAltCat P) . j,k and
A3: h in the Arrows of (POSAltCat P) . k,l ; :: thesis: (the Comp of (POSAltCat P) . i,k,l) . h,((the Comp of (POSAltCat P) . i,j,k) . g,f) = (the Comp of (POSAltCat P) . i,j,l) . ((the Comp of (POSAltCat P) . j,k,l) . h,g),f
A4: g in MonFuncs j9,k9 by A2, Def9;
A5: h in MonFuncs k9,l9 by A3, Def9;
A6: f in MonFuncs i9,j9 by A1, Def9;
then reconsider f9 = f, g9 = g, h9 = h as Function by A4, A5;
A7: the Comp of (POSAltCat P) . i,j,l = FuncComp (MonFuncs i9,j9),(MonFuncs j9,l9) by Def9;
the Comp of (POSAltCat P) . j,k,l = FuncComp (MonFuncs j9,k9),(MonFuncs k9,l9) by Def9;
then A8: (the Comp of (POSAltCat P) . j,k,l) . h,g = h9 * g9 by A4, A5, ALTCAT_1:13;
the Comp of (POSAltCat P) . i,j,k = FuncComp (MonFuncs i9,j9),(MonFuncs j9,k9) by Def9;
then A9: (the Comp of (POSAltCat P) . i,j,k) . g,f = g9 * f9 by A6, A4, ALTCAT_1:13;
h9 * g9 in MonFuncs j9,l9 by A4, A5, Th6;
then A10: (the Comp of (POSAltCat P) . i,j,l) . (h9 * g9),f9 = (h9 * g9) * f9 by A6, A7, ALTCAT_1:13;
A11: the Comp of (POSAltCat P) . i,k,l = FuncComp (MonFuncs i9,k9),(MonFuncs k9,l9) by Def9;
g9 * f9 in MonFuncs i9,k9 by A6, A4, Th6;
then (the Comp of (POSAltCat P) . i,k,l) . h,(g9 * f9) = h9 * (g9 * f9) by A5, A11, ALTCAT_1:13;
hence (the Comp of (POSAltCat P) . i,k,l) . h,((the Comp of (POSAltCat P) . i,j,k) . g,f) = (the Comp of (POSAltCat P) . i,j,l) . ((the Comp of (POSAltCat P) . j,k,l) . h,g),f by A9, A8, A10, RELAT_1:55; :: thesis: verum

end;

thus the Comp of (POSAltCat P) is with_left_units :: according to ALTCAT_1:def 18 :: thesis: the Comp of (POSAltCat P) is with_right_units

proof

let j be Element of (POSAltCat P); :: according to ALTCAT_1:def 9 :: thesis: ex b₁ being set st
( b₁ in the Arrows of (POSAltCat P) . j,j & ( for b₂ being Element of the carrier of (POSAltCat P)
for b₃ being set holds
( not b₃ in the Arrows of (POSAltCat P) . b₂,j or (the Comp of (POSAltCat P) . b₂,j,j) . b₁,b₃ = b₃ ) ) )
reconsider j9 = j as Element of P by Def9;
take e = id the carrier of j9; :: thesis: ( e in the Arrows of (POSAltCat P) . j,j & ( for b₁ being Element of the carrier of (POSAltCat P)
for b₂ being set holds
( not b₂ in the Arrows of (POSAltCat P) . b₁,j or (the Comp of (POSAltCat P) . b₁,j,j) . e,b₂ = b₂ ) ) )
the Arrows of (POSAltCat P) . j,j = MonFuncs j9,j9 by Def9;
hence e in the Arrows of (POSAltCat P) . j,j by Th7; :: thesis: for b₁ being Element of the carrier of (POSAltCat P)
for b₂ being set holds
( not b₂ in the Arrows of (POSAltCat P) . b₁,j or (the Comp of (POSAltCat P) . b₁,j,j) . e,b₂ = b₂ )
let i be Element of (POSAltCat P); :: thesis: for b₁ being set holds
( not b₁ in the Arrows of (POSAltCat P) . i,j or (the Comp of (POSAltCat P) . i,j,j) . e,b₁ = b₁ )
let f be set ; :: thesis: ( not f in the Arrows of (POSAltCat P) . i,j or (the Comp of (POSAltCat P) . i,j,j) . e,f = f )
reconsider i9 = i as Element of P by Def9;
A12: the Comp of (POSAltCat P) . i,j,j = FuncComp (MonFuncs i9,j9),(MonFuncs j9,j9) by Def9;
assume f in the Arrows of (POSAltCat P) . i,j ; :: thesis: (the Comp of (POSAltCat P) . i,j,j) . e,f = f
then A13: f in MonFuncs i9,j9 by Def9;
then consider f9 being Function of i9,j9 such that
A14: f = f9 and
f9 in Funcs the carrier of i9,the carrier of j9 and
f9 is monotone by Def6;
A15: e in MonFuncs j9,j9 by Th7;
then consider e9 being Function of j9,j9 such that
A16: e = e9 and
e9 in Funcs the carrier of j9,the carrier of j9 and
e9 is monotone by Def6;
rng f9 c= the carrier of j9 ;
then e9 * f9 = f by A16, A14, RELAT_1:79;
hence (the Comp of (POSAltCat P) . i,j,j) . e,f = f by A15, A16, A13, A14, A12, ALTCAT_1:13; :: thesis: verum

end;

thus the Comp of (POSAltCat P) is with_right_units :: thesis: verum

proof

let i be Element of (POSAltCat P); :: according to ALTCAT_1:def 8 :: thesis: ex b₁ being set st
( b₁ in the Arrows of (POSAltCat P) . i,i & ( for b₂ being Element of the carrier of (POSAltCat P)
for b₃ being set holds
( not b₃ in the Arrows of (POSAltCat P) . i,b₂ or (the Comp of (POSAltCat P) . i,i,b₂) . b₃,b₁ = b₃ ) ) )
reconsider i9 = i as Element of P by Def9;
take e = id the carrier of i9; :: thesis: ( e in the Arrows of (POSAltCat P) . i,i & ( for b₁ being Element of the carrier of (POSAltCat P)
for b₂ being set holds
( not b₂ in the Arrows of (POSAltCat P) . i,b₁ or (the Comp of (POSAltCat P) . i,i,b₁) . b₂,e = b₂ ) ) )
the Arrows of (POSAltCat P) . i,i = MonFuncs i9,i9 by Def9;
hence e in the Arrows of (POSAltCat P) . i,i by Th7; :: thesis: for b₁ being Element of the carrier of (POSAltCat P)
for b₂ being set holds
( not b₂ in the Arrows of (POSAltCat P) . i,b₁ or (the Comp of (POSAltCat P) . i,i,b₁) . b₂,e = b₂ )
let j be Element of (POSAltCat P); :: thesis: for b₁ being set holds
( not b₁ in the Arrows of (POSAltCat P) . i,j or (the Comp of (POSAltCat P) . i,i,j) . b₁,e = b₁ )
let f be set ; :: thesis: ( not f in the Arrows of (POSAltCat P) . i,j or (the Comp of (POSAltCat P) . i,i,j) . f,e = f )
reconsider j9 = j as Element of P by Def9;
A17: the Comp of (POSAltCat P) . i,i,j = FuncComp (MonFuncs i9,i9),(MonFuncs i9,j9) by Def9;
assume f in the Arrows of (POSAltCat P) . i,j ; :: thesis: (the Comp of (POSAltCat P) . i,i,j) . f,e = f
then A18: f in MonFuncs i9,j9 by Def9;
then consider f9 being Function of i9,j9 such that
A19: f = f9 and
f9 in Funcs the carrier of i9,the carrier of j9 and
f9 is monotone by Def6;
A20: e in MonFuncs i9,i9 by Th7;
then consider e9 being Function of i9,i9 such that
A21: e = e9 and
e9 in Funcs the carrier of i9,the carrier of i9 and
e9 is monotone by Def6;
dom f9 = the carrier of i9 by FUNCT_2:def 1;
then f9 * e9 = f by A21, A19, RELAT_1:78;
hence (the Comp of (POSAltCat P) . i,i,j) . f,e = f by A20, A21, A18, A19, A17, ALTCAT_1:13; :: thesis: verum

end;