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 ; :: 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 i' = i, j' = j, k' = k, l' = 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 j',k' by A2, Def9;
A5: h in MonFuncs k',l' by A3, Def9;
A6: f in MonFuncs i',j' by A1, Def9;
then reconsider f' = f, g' = g, h' = h as Function by A4, A5;
A7: the Comp of (POSAltCat P) . i,j,l = FuncComp (MonFuncs i',j'),(MonFuncs j',l') by Def9;
the Comp of (POSAltCat P) . j,k,l = FuncComp (MonFuncs j',k'),(MonFuncs k',l') by Def9;
then A8: (the Comp of (POSAltCat P) . j,k,l) . h,g = h' * g' by A4, A5, ALTCAT_1:13;
the Comp of (POSAltCat P) . i,j,k = FuncComp (MonFuncs i',j'),(MonFuncs j',k') by Def9;
then A9: (the Comp of (POSAltCat P) . i,j,k) . g,f = g' * f' by A6, A4, ALTCAT_1:13;
h' * g' in MonFuncs j',l' by A4, A5, Th6;
then A10: (the Comp of (POSAltCat P) . i,j,l) . (h' * g'),f' = (h' * g') * f' by A6, A7, ALTCAT_1:13;
A11: the Comp of (POSAltCat P) . i,k,l = FuncComp (MonFuncs i',k'),(MonFuncs k',l') by Def9;
g' * f' in MonFuncs i',k' by A6, A4, Th6;
then (the Comp of (POSAltCat P) . i,k,l) . h,(g' * f') = h' * (g' * f') 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 ; :: 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 j' = j as Element of P by Def9;
take e = id the carrier of j'; :: 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 j',j' 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 ; :: 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 i' = i as Element of P by Def9;
A12: the Comp of (POSAltCat P) . i,j,j = FuncComp (MonFuncs i',j'),(MonFuncs j',j') 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 i',j' by Def9;
then consider f' being Function of i',j' such that
A14: f = f' and
f' in Funcs the carrier of i',the carrier of j' and
f' is monotone by Def6;
A15: e in MonFuncs j',j' by Th7;
then consider e' being Function of j',j' such that
A16: e = e' and
e' in Funcs the carrier of j',the carrier of j' and
e' is monotone by Def6;
rng f' c= the carrier of j' ;
then e' * f' = 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 ; :: 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 i' = i as Element of P by Def9;
take e = id the carrier of i'; :: 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 i',i' 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 ; :: 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 j' = j as Element of P by Def9;
A17: the Comp of (POSAltCat P) . i,i,j = FuncComp (MonFuncs i',i'),(MonFuncs i',j') 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 i',j' by Def9;
then consider f' being Function of i',j' such that
A19: f = f' and
f' in Funcs the carrier of i',the carrier of j' and
f' is monotone by Def6;
A20: e in MonFuncs i',i' by Th7;
then consider e' being Function of i',i' such that
A21: e = e' and
e' in Funcs the carrier of i',the carrier of i' and
e' is monotone by Def6;
dom f' = the carrier of i' by FUNCT_2:def 1;
then f' * e' = 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;