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
ALTCAT_1:def 15 POSAltCat P is with_units proof
let i,
j,
k,
l be
Element of
(POSAltCat P);
ALTCAT_1:def 5 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 ;
( 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)
;
( 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;
verum
end;
thus
the Comp of (POSAltCat P) is with_left_units
ALTCAT_1:def 16 the Comp of (POSAltCat P) is with_right_units proof
let j be
Element of
(POSAltCat P);
ALTCAT_1:def 7 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;
( 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;
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);
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 ;
( 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)
;
( 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;
verum
end;
thus
the Comp of (POSAltCat P) is with_right_units
verumproof
let i be
Element of
(POSAltCat P);
ALTCAT_1:def 6 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;
( 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;
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);
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 ;
( 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)
;
( 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;
verum
end;