set M = MSAlgCat (S,A);
set G = MSAlgCat (S,A);
set GM = the Arrows of (MSAlgCat (S,A));
set C = the Comp of (MSAlgCat (S,A));
thus
MSAlgCat (S,A) is transitive
( MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )proof
let o1,
o2,
o3 be
Object of
(MSAlgCat (S,A));
ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o19 =
o1,
o29 =
o2,
o39 =
o3 as
Element of
MSAlg_set (
S,
A)
by Def4;
assume that A1:
<^o1,o2^> <> {}
and A2:
<^o2,o3^> <> {}
;
not <^o1,o3^> = {}
set t = the
Element of
MSAlg_morph (
S,
A,
o19,
o29);
MSAlg_morph (
S,
A,
o19,
o29)
<> {}
by A1, Def4;
then consider M,
N being
strict feasible MSAlgebra over
S,
f being
ManySortedFunction of
M,
N such that A3:
M = o19
and A4:
N = o29
and
f = the
Element of
MSAlg_morph (
S,
A,
o19,
o29)
and A5:
the
Sorts of
M is_transformable_to the
Sorts of
N
and A6:
f is_homomorphism M,
N
by Def3;
set s = the
Element of
MSAlg_morph (
S,
A,
o29,
o39);
MSAlg_morph (
S,
A,
o29,
o39)
<> {}
by A2, Def4;
then consider M1,
N1 being
strict feasible MSAlgebra over
S,
g being
ManySortedFunction of
M1,
N1 such that A7:
M1 = o29
and A8:
N1 = o39
and
g = the
Element of
MSAlg_morph (
S,
A,
o29,
o39)
and A9:
the
Sorts of
M1 is_transformable_to the
Sorts of
N1
and A10:
g is_homomorphism M1,
N1
by Def3;
reconsider g9 =
g as
ManySortedFunction of
N,
N1 by A4, A7;
consider GF being
ManySortedFunction of
M,
N1 such that
GF = g9 ** f
and A11:
GF is_homomorphism M,
N1
by A4, A5, A6, A7, A9, A10, Th5;
the
Sorts of
M is_transformable_to the
Sorts of
N1
by A4, A5, A7, A9, AUTALG_1:10;
then
GF in MSAlg_morph (
S,
A,
o19,
o39)
by A3, A8, A11, Def3;
hence
not
<^o1,o3^> = {}
by Def4;
verum
end;
thus
the Comp of (MSAlgCat (S,A)) is associative
ALTCAT_1:def 15 MSAlgCat (S,A) is with_units proof
let i,
j,
k,
l be
Element of
(MSAlgCat (S,A));
ALTCAT_1:def 5 for b1, b2, b3 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or not b2 in the Arrows of (MSAlgCat (S,A)) . (j,k) or not b3 in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (b3,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (b3,b2)),b1) )let f,
g,
h be
set ;
( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or not g in the Arrows of (MSAlgCat (S,A)) . (j,k) or not h in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) )
reconsider i9 =
i,
j9 =
j,
k9 =
k,
l9 =
l as
Element of
MSAlg_set (
S,
A)
by Def4;
assume that A12:
f in the
Arrows of
(MSAlgCat (S,A)) . (
i,
j)
and A13:
g in the
Arrows of
(MSAlgCat (S,A)) . (
j,
k)
and A14:
h in the
Arrows of
(MSAlgCat (S,A)) . (
k,
l)
;
( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f)
g in MSAlg_morph (
S,
A,
j9,
k9)
by A13, Def4;
then consider M2,
N2 being
strict feasible MSAlgebra over
S,
G being
ManySortedFunction of
M2,
N2 such that A15:
M2 = j9
and A16:
N2 = k9
and A17:
g = G
and A18:
the
Sorts of
M2 is_transformable_to the
Sorts of
N2
and A19:
G is_homomorphism M2,
N2
by Def3;
h in MSAlg_morph (
S,
A,
k9,
l9)
by A14, Def4;
then consider M3,
N3 being
strict feasible MSAlgebra over
S,
H being
ManySortedFunction of
M3,
N3 such that A20:
M3 = k9
and A21:
N3 = l9
and A22:
h = H
and A23:
the
Sorts of
M3 is_transformable_to the
Sorts of
N3
and A24:
H is_homomorphism M3,
N3
by Def3;
reconsider G9 =
G as
ManySortedFunction of
M2,
M3 by A16, A20;
consider HG being
ManySortedFunction of
M2,
N3 such that A25:
HG = H ** G9
and A26:
HG is_homomorphism M2,
N3
by A16, A18, A19, A20, A23, A24, Th5;
A27:
( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (
H,
G)
= H ** G9
by A13, A14, A17, A22, Def4;
f in MSAlg_morph (
S,
A,
i9,
j9)
by A12, Def4;
then consider M1,
N1 being
strict feasible MSAlgebra over
S,
F being
ManySortedFunction of
M1,
N1 such that A28:
M1 = i9
and A29:
N1 = j9
and A30:
f = F
and A31:
the
Sorts of
M1 is_transformable_to the
Sorts of
N1
and A32:
F is_homomorphism M1,
N1
by Def3;
A33:
( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (
g,
f)
= G ** F
by A12, A13, A30, A17, Def4;
consider GF being
ManySortedFunction of
M1,
M3 such that A34:
GF = G9 ** F
and A35:
GF is_homomorphism M1,
M3
by A29, A31, A32, A15, A16, A18, A19, A20, Th5;
the
Sorts of
M1 is_transformable_to the
Sorts of
M3
by A29, A31, A15, A16, A18, A20, AUTALG_1:10;
then
G9 ** F in MSAlg_morph (
S,
A,
i9,
k9)
by A28, A20, A34, A35, Def3;
then
GF in the
Arrows of
(MSAlgCat (S,A)) . (
i,
k)
by A34, Def4;
then A36:
( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (
H,
GF)
= H ** GF
by A14, A22, Def4;
the
Sorts of
M2 is_transformable_to the
Sorts of
N3
by A16, A18, A20, A23, AUTALG_1:10;
then
HG in MSAlg_morph (
S,
A,
j9,
l9)
by A15, A21, A26, Def3;
then A37:
H ** G9 in the
Arrows of
(MSAlgCat (S,A)) . (
j,
l)
by A25, Def4;
(H ** G9) ** F = H ** (G9 ** F)
by PBOOLE:140;
hence
( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (
h,
(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f)))
= ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . (
(( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),
f)
by A12, A30, A17, A22, A33, A34, A36, A27, A37, Def4;
verum
end;
thus
the Comp of (MSAlgCat (S,A)) is with_left_units
ALTCAT_1:def 16 the Comp of (MSAlgCat (S,A)) is with_right_units proof
let j be
Element of
(MSAlgCat (S,A));
ALTCAT_1:def 7 ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (b2,j) or ( the Comp of (MSAlgCat (S,A)) . (b2,j,j)) . (b1,b3) = b3 ) ) )
reconsider j9 =
j as
Element of
MSAlg_set (
S,
A)
by Def4;
consider MS being
strict feasible MSAlgebra over
S such that A38:
MS = j9
and
for
C being
Component of the
Sorts of
MS holds
C c= A
by Def2;
reconsider e =
id the
Sorts of
MS as
ManySortedFunction of
MS,
MS ;
take
e
;
( e in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 ) ) )
(
e is_homomorphism MS,
MS & the
Arrows of
(MSAlgCat (S,A)) . (
j,
j)
= MSAlg_morph (
S,
A,
j9,
j9) )
by Def4, MSUALG_3:9;
hence A39:
e in the
Arrows of
(MSAlgCat (S,A)) . (
j,
j)
by A38, Def3;
for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 )
let i be
Element of
(MSAlgCat (S,A));
for b1 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,b1) = b1 )
reconsider i9 =
i as
Element of
MSAlg_set (
S,
A)
by Def4;
let f be
set ;
( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f )
reconsider I =
i,
J =
j as
Object of
(MSAlgCat (S,A)) ;
assume A40:
f in the
Arrows of
(MSAlgCat (S,A)) . (
i,
j)
;
( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f
then
f in MSAlg_morph (
S,
A,
i9,
j9)
by Def4;
then consider M1,
N1 being
strict feasible MSAlgebra over
S,
F being
ManySortedFunction of
M1,
N1 such that
M1 = i9
and A41:
N1 = j9
and A42:
F = f
and
the
Sorts of
M1 is_transformable_to the
Sorts of
N1
and
F is_homomorphism M1,
N1
by Def3;
reconsider F =
F as
ManySortedFunction of
M1,
MS by A38, A41;
( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (
e,
f)
= e ** F
by A39, A40, A42, Def4;
hence
( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (
e,
f)
= f
by A42, MSUALG_3:4;
verum
end;
thus
the Comp of (MSAlgCat (S,A)) is with_right_units
verumproof
let i be
Element of
(MSAlgCat (S,A));
ALTCAT_1:def 6 ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (i,b2) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider i9 =
i as
Element of
MSAlg_set (
S,
A)
by Def4;
consider MS being
strict feasible MSAlgebra over
S such that A43:
MS = i9
and
for
C being
Component of the
Sorts of
MS holds
C c= A
by Def2;
reconsider e =
id the
Sorts of
MS as
ManySortedFunction of
MS,
MS ;
take
e
;
( e in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 ) ) )
(
e is_homomorphism MS,
MS & the
Arrows of
(MSAlgCat (S,A)) . (
i,
i)
= MSAlg_morph (
S,
A,
i9,
i9) )
by Def4, MSUALG_3:9;
hence A44:
e in the
Arrows of
(MSAlgCat (S,A)) . (
i,
i)
by A43, Def3;
for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 )
let j be
Element of
(MSAlgCat (S,A));
for b1 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (b1,e) = b1 )
reconsider j9 =
j as
Element of
MSAlg_set (
S,
A)
by Def4;
let f be
set ;
( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f )
reconsider I =
i,
J =
j as
Object of
(MSAlgCat (S,A)) ;
assume A45:
f in the
Arrows of
(MSAlgCat (S,A)) . (
i,
j)
;
( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f
then
f in MSAlg_morph (
S,
A,
i9,
j9)
by Def4;
then consider M1,
N1 being
strict feasible MSAlgebra over
S,
F being
ManySortedFunction of
M1,
N1 such that A46:
M1 = i9
and
N1 = j9
and A47:
F = f
and
the
Sorts of
M1 is_transformable_to the
Sorts of
N1
and
F is_homomorphism M1,
N1
by Def3;
reconsider F =
F as
ManySortedFunction of
MS,
N1 by A43, A46;
( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (
f,
e)
= F ** e
by A44, A45, A47, Def4;
hence
( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (
f,
e)
= f
by A47, MSUALG_3:3;
verum
end;