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
proof
let i, j, k, l be Element of (POSAltCat P); :: according to ALTCAT_1:def 5 :: thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or not b2 in the Arrows of (POSAltCat P) . (j,k) or not b3 in the Arrows of (POSAltCat P) . (k,l) or ( the Comp of (POSAltCat P) . (i,k,l)) . (b3,(( the Comp of (POSAltCat P) . (i,j,k)) . (b2,b1))) = ( the Comp of (POSAltCat P) . (i,j,l)) . ((( the Comp of (POSAltCat P) . (j,k,l)) . (b3,b2)),b1) )
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;
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
proof
let j be Element of (POSAltCat P); :: according to ALTCAT_1:def 7 :: thesis: ex b1 being set st
( b1 in the Arrows of (POSAltCat P) . (j,j) & ( for b2 being Element of the carrier of (POSAltCat P)
for b3 being set holds
( not b3 in the Arrows of (POSAltCat P) . (b2,j) or ( the Comp of (POSAltCat P) . (b2,j,j)) . (b1,b3) = b3 ) ) )
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 b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 ) ) )
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 b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (b1,j) or ( the Comp of (POSAltCat P) . (b1,j,j)) . (e,b2) = b2 )
let i be Element of (POSAltCat P); :: thesis: for b1 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,j,j)) . (e,b1) = b1 )
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;
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 6 :: thesis: ex b1 being set st
( b1 in the Arrows of (POSAltCat P) . (i,i) & ( for b2 being Element of the carrier of (POSAltCat P)
for b3 being set holds
( not b3 in the Arrows of (POSAltCat P) . (i,b2) or ( the Comp of (POSAltCat P) . (i,i,b2)) . (b3,b1) = b3 ) ) )
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 b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 ) ) )
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 b1 being Element of the carrier of (POSAltCat P)
for b2 being set holds
( not b2 in the Arrows of (POSAltCat P) . (i,b1) or ( the Comp of (POSAltCat P) . (i,i,b1)) . (b2,e) = b2 )
let j be Element of (POSAltCat P); :: thesis: for b1 being set holds
( not b1 in the Arrows of (POSAltCat P) . (i,j) or ( the Comp of (POSAltCat P) . (i,i,j)) . (b1,e) = b1 )
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;