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 15 :: thesis: POSAltCat P is with_units

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 15 :: thesis: POSAltCat P is with_units

proof

thus
the Comp of (POSAltCat P) is with_left_units
:: according to ALTCAT_1:def 16 :: thesis: the Comp of (POSAltCat P) is with_right_units
let i, j, k, l be Element of (POSAltCat P); :: according to ALTCAT_1:def 5 :: thesis: for b_{1}, b_{2}, b_{3} being set holds

( not b_{1} in the Arrows of (POSAltCat P) . (i,j) or not b_{2} in the Arrows of (POSAltCat P) . (j,k) or not b_{3} in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (b_{3},(( the Comp of (POSAltCat P) . (i,j,k)) . (b_{2},b_{1}))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (b_{3},b_{2})),b_{1}) )

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:11;

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:11;

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:11;

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:11;

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

end;( not 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:11;

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:11;

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:11;

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:11;

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

proof

thus
the Comp of (POSAltCat P) is with_right_units
:: thesis: verum
let j be Element of (POSAltCat P); :: according to ALTCAT_1:def 7 :: thesis: ex b_{1} being set st

( b_{1} in the Arrows of (POSAltCat P) . (j,j) & ( for b_{2} being Element of the carrier of (POSAltCat P)

for b_{3} being set holds

( not b_{3} in the Arrows of (POSAltCat P) . (b_{2},j) or ( the Comp of (POSAltCat P) . (b_{2},j,j)) . (b_{1},b_{3}) = b_{3} ) ) )

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_{1} being Element of the carrier of (POSAltCat P)

for b_{2} being set holds

( not b_{2} in the Arrows of (POSAltCat P) . (b_{1},j) or ( the Comp of (POSAltCat P) . (b_{1},j,j)) . (e,b_{2}) = b_{2} ) ) )

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_{1} being Element of the carrier of (POSAltCat P)

for b_{2} being set holds

( not b_{2} in the Arrows of (POSAltCat P) . (b_{1},j) or ( the Comp of (POSAltCat P) . (b_{1},j,j)) . (e,b_{2}) = b_{2} )

let i be Element of (POSAltCat P); :: thesis: for b_{1} being set holds

( not b_{1} in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,b_{1}) = b_{1} )

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:53;

hence ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f by A15, A16, A13, A14, A12, ALTCAT_1:11; :: thesis: verum

end;( b

for b

( not 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

for b

( not 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

for b

( not b

let i be Element of (POSAltCat P); :: thesis: for b

( not 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:53;

hence ( the Comp of (POSAltCat P) . (i,j,j)) . (e,f) = f by A15, A16, A13, A14, A12, ALTCAT_1:11; :: thesis: verum

proof

let i be Element of (POSAltCat P); :: according to ALTCAT_1:def 6 :: thesis: ex b_{1} being set st

( b_{1} in the Arrows of (POSAltCat P) . (i,i) & ( for b_{2} being Element of the carrier of (POSAltCat P)

for b_{3} being set holds

( not b_{3} in the Arrows of (POSAltCat P) . (i,b_{2}) or ( the Comp of (POSAltCat P) . (i,i,b_{2})) . (b_{3},b_{1}) = b_{3} ) ) )

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_{1} being Element of the carrier of (POSAltCat P)

for b_{2} being set holds

( not b_{2} in the Arrows of (POSAltCat P) . (i,b_{1}) or ( the Comp of (POSAltCat P) . (i,i,b_{1})) . (b_{2},e) = b_{2} ) ) )

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_{1} being Element of the carrier of (POSAltCat P)

for b_{2} being set holds

( not b_{2} in the Arrows of (POSAltCat P) . (i,b_{1}) or ( the Comp of (POSAltCat P) . (i,i,b_{1})) . (b_{2},e) = b_{2} )

let j be Element of (POSAltCat P); :: thesis: for b_{1} being set holds

( not b_{1} in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (b_{1},e) = b_{1} )

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:52;

hence ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f by A20, A21, A18, A19, A17, ALTCAT_1:11; :: thesis: verum

end;( b

for b

( not 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

for b

( not 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

for b

( not b

let j be Element of (POSAltCat P); :: thesis: for b

( not 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:52;

hence ( the Comp of (POSAltCat P) . (i,i,j)) . (f,e) = f by A20, A21, A18, A19, A17, ALTCAT_1:11; :: thesis: verum