set G = MSAlgCat S,A;
thus
MSAlgCat S,A is transitive
:: thesis: ( MSAlgCat S,A is associative & MSAlgCat S,A is with_units )proof
let o1,
o2,
o3 be
object of
(MSAlgCat S,A);
:: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o1' =
o1,
o2' =
o2,
o3' =
o3 as
Element of
MSAlg_set S,
A by Def4;
assume
(
<^o1,o2^> <> {} &
<^o2,o3^> <> {} )
;
:: thesis: not <^o1,o3^> = {}
then A1:
(
MSAlg_morph S,
A,
o1',
o2' <> {} &
MSAlg_morph S,
A,
o2',
o3' <> {} )
by Def4;
consider t being
Element of
MSAlg_morph S,
A,
o1',
o2';
consider s being
Element of
MSAlg_morph S,
A,
o2',
o3';
consider M,
N being
strict feasible MSAlgebra of
S,
f being
ManySortedFunction of
M,
N such that A2:
(
M = o1' &
N = o2' &
f = t & the
Sorts of
M is_transformable_to the
Sorts of
N &
f is_homomorphism M,
N )
by A1, Def3;
consider M1,
N1 being
strict feasible MSAlgebra of
S,
g being
ManySortedFunction of
M1,
N1 such that A3:
(
M1 = o2' &
N1 = o3' &
g = s & the
Sorts of
M1 is_transformable_to the
Sorts of
N1 &
g is_homomorphism M1,
N1 )
by A1, Def3;
A4:
the
Sorts of
M is_transformable_to the
Sorts of
N1
by A2, A3, AUTALG_1:11;
reconsider g' =
g as
ManySortedFunction of
N,
N1 by A2, A3;
consider GF being
ManySortedFunction of
M,
N1 such that A5:
(
GF = g' ** f &
GF is_homomorphism M,
N1 )
by A2, A3, Th5;
GF in MSAlg_morph S,
A,
o1',
o3'
by A2, A3, A4, A5, Def3;
hence
not
<^o1,o3^> = {}
by Def4;
:: thesis: verum
end;
set M = MSAlgCat S,A;
set GM = the Arrows of (MSAlgCat S,A);
set C = the Comp of (MSAlgCat S,A);
thus
the Comp of (MSAlgCat S,A) is associative
:: according to ALTCAT_1:def 17 :: thesis: MSAlgCat S,A is with_units proof
let i,
j,
k,
l be
Element of
(MSAlgCat S,A);
:: according to ALTCAT_1:def 7 :: thesis: 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 )
reconsider i' =
i,
j' =
j,
k' =
k,
l' =
l as
Element of
MSAlg_set S,
A by Def4;
let f,
g,
h be
set ;
:: thesis: ( 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 )
assume A6:
(
f in the
Arrows of
(MSAlgCat S,A) . i,
j &
g in the
Arrows of
(MSAlgCat S,A) . j,
k &
h in the
Arrows of
(MSAlgCat S,A) . k,
l )
;
:: thesis: (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
then A7:
(
f in MSAlg_morph S,
A,
i',
j' &
g in MSAlg_morph S,
A,
j',
k' &
h in MSAlg_morph S,
A,
k',
l' )
by Def4;
then consider M1,
N1 being
strict feasible MSAlgebra of
S,
F being
ManySortedFunction of
M1,
N1 such that A8:
(
M1 = i' &
N1 = j' &
f = F & the
Sorts of
M1 is_transformable_to the
Sorts of
N1 &
F is_homomorphism M1,
N1 )
by Def3;
consider M2,
N2 being
strict feasible MSAlgebra of
S,
G being
ManySortedFunction of
M2,
N2 such that A9:
(
M2 = j' &
N2 = k' &
g = G & the
Sorts of
M2 is_transformable_to the
Sorts of
N2 &
G is_homomorphism M2,
N2 )
by A7, Def3;
consider M3,
N3 being
strict feasible MSAlgebra of
S,
H being
ManySortedFunction of
M3,
N3 such that A10:
(
M3 = k' &
N3 = l' &
h = H & the
Sorts of
M3 is_transformable_to the
Sorts of
N3 &
H is_homomorphism M3,
N3 )
by A7, Def3;
A11:
the
Sorts of
M1 is_transformable_to the
Sorts of
M3
by A8, A9, A10, AUTALG_1:11;
A12:
the
Sorts of
M2 is_transformable_to the
Sorts of
N3
by A9, A10, AUTALG_1:11;
reconsider G' =
G as
ManySortedFunction of
M2,
M3 by A9, A10;
A13:
(the Comp of (MSAlgCat S,A) . i,j,k) . g,
f = G ** F
by A6, A8, A9, Def4;
consider GF being
ManySortedFunction of
M1,
M3 such that A14:
(
GF = G' ** F &
GF is_homomorphism M1,
M3 )
by A8, A9, A10, Th5;
G' ** F in MSAlg_morph S,
A,
i',
k'
by A8, A10, A11, A14, Def3;
then
GF in the
Arrows of
(MSAlgCat S,A) . i,
k
by A14, Def4;
then A15:
(the Comp of (MSAlgCat S,A) . i,k,l) . H,
GF = H ** GF
by A6, A10, Def4;
A16:
(the Comp of (MSAlgCat S,A) . j,k,l) . H,
G = H ** G'
by A6, A9, A10, Def4;
consider HG being
ManySortedFunction of
M2,
N3 such that A17:
(
HG = H ** G' &
HG is_homomorphism M2,
N3 )
by A9, A10, Th5;
HG in MSAlg_morph S,
A,
j',
l'
by A9, A10, A12, A17, Def3;
then A18:
H ** G' in the
Arrows of
(MSAlgCat S,A) . j,
l
by A17, Def4;
(H ** G') ** F = H ** (G' ** F)
by PBOOLE:154;
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 A6, A8, A9, A10, A13, A14, A15, A16, A18, Def4;
:: thesis: verum
end;
thus
the Comp of (MSAlgCat S,A) is with_left_units
:: according to ALTCAT_1:def 18 :: thesis: the Comp of (MSAlgCat S,A) is with_right_units proof
let j be
Element of
(MSAlgCat S,A);
:: according to ALTCAT_1:def 9 :: thesis: 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 j' =
j as
Element of
MSAlg_set S,
A by Def4;
consider MS being
strict feasible MSAlgebra of
S such that A19:
(
MS = j' & ( 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 ;
A20:
e is_homomorphism MS,
MS
by MSUALG_3:9;
take
e
;
:: thesis: ( 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 ) ) )
the
Arrows of
(MSAlgCat S,A) . j,
j = MSAlg_morph S,
A,
j',
j'
by Def4;
hence A21:
e in the
Arrows of
(MSAlgCat S,A) . j,
j
by A19, A20, Def3;
:: thesis: 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);
:: thesis: 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 )let f be
set ;
:: thesis: ( 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 as
Element of
MSAlg_set S,
A by Def4;
assume A22:
f in the
Arrows of
(MSAlgCat S,A) . i,
j
;
:: thesis: (the Comp of (MSAlgCat S,A) . i,j,j) . e,f = f
then
f in MSAlg_morph S,
A,
i',
j'
by Def4;
then consider M1,
N1 being
strict feasible MSAlgebra of
S,
F being
ManySortedFunction of
M1,
N1 such that A23:
(
M1 = i' &
N1 = j' &
F = f & the
Sorts of
M1 is_transformable_to the
Sorts of
N1 &
F is_homomorphism M1,
N1 )
by Def3;
reconsider F =
F as
ManySortedFunction of
M1,
MS by A19, A23;
reconsider I =
i,
J =
j as
object of
(MSAlgCat S,A) ;
(the Comp of (MSAlgCat S,A) . I,J,J) . e,
f = e ** F
by A21, A22, A23, Def4;
hence
(the Comp of (MSAlgCat S,A) . i,j,j) . e,
f = f
by A23, MSUALG_3:4;
:: thesis: verum
end;
thus
the Comp of (MSAlgCat S,A) is with_right_units
:: thesis: verumproof
let i be
Element of
(MSAlgCat S,A);
:: according to ALTCAT_1:def 8 :: thesis: 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 i' =
i as
Element of
MSAlg_set S,
A by Def4;
consider MS being
strict feasible MSAlgebra of
S such that A24:
(
MS = i' & ( 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 ;
A25:
e is_homomorphism MS,
MS
by MSUALG_3:9;
take
e
;
:: thesis: ( 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 ) ) )
the
Arrows of
(MSAlgCat S,A) . i,
i = MSAlg_morph S,
A,
i',
i'
by Def4;
hence A26:
e in the
Arrows of
(MSAlgCat S,A) . i,
i
by A24, A25, Def3;
:: thesis: 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);
:: thesis: 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 )let f be
set ;
:: thesis: ( 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 j' =
j as
Element of
MSAlg_set S,
A by Def4;
assume A27:
f in the
Arrows of
(MSAlgCat S,A) . i,
j
;
:: thesis: (the Comp of (MSAlgCat S,A) . i,i,j) . f,e = f
then
f in MSAlg_morph S,
A,
i',
j'
by Def4;
then consider M1,
N1 being
strict feasible MSAlgebra of
S,
F being
ManySortedFunction of
M1,
N1 such that A28:
(
M1 = i' &
N1 = j' &
F = f & the
Sorts of
M1 is_transformable_to the
Sorts of
N1 &
F is_homomorphism M1,
N1 )
by Def3;
reconsider F =
F as
ManySortedFunction of
MS,
N1 by A24, A28;
reconsider I =
i,
J =
j as
object of
(MSAlgCat S,A) ;
(the Comp of (MSAlgCat S,A) . I,I,J) . f,
e = F ** e
by A26, A27, A28, Def4;
hence
(the Comp of (MSAlgCat S,A) . i,i,j) . f,
e = f
by A28, MSUALG_3:3;
:: thesis: verum
end;