set c = MSAlg_set (S,A);
deffunc H1( Element of MSAlg_set (S,A), Element of MSAlg_set (S,A)) -> set = MSAlg_morph (S,A,$1,$2);
consider M being ManySortedSet of [:(MSAlg_set (S,A)),(MSAlg_set (S,A)):] such that
A1:
for i, j being Element of MSAlg_set (S,A) holds M . (i,j) = H1(i,j)
from ALTCAT_1:sch 2();
defpred S1[ object , object , object ] means ex i, j, k being Element of MSAlg_set (S,A) st
( $3 = [i,j,k] & ( for f, g being Function-yielding Function st f in M . (i,j) & g in M . (j,k) & $2 = [g,f] holds
$1 = g ** f ) );
A2:
for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds
for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
proof
let ijk be
object ;
( ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] implies for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] ) )
assume
ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):]
;
for x being object st x in {|M,M|} . ijk holds
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
then consider x1,
x2,
x3 being
object such that A3:
(
x1 in MSAlg_set (
S,
A) &
x2 in MSAlg_set (
S,
A) &
x3 in MSAlg_set (
S,
A) )
and A4:
ijk = [x1,x2,x3]
by MCART_1:68;
reconsider x1 =
x1,
x2 =
x2,
x3 =
x3 as
Element of
MSAlg_set (
S,
A)
by A3;
let x be
object ;
( x in {|M,M|} . ijk implies ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] ) )
A5:
(
{|M,M|} . (
x1,
x2,
x3)
= {|M,M|} . [x1,x2,x3] &
{|M,M|} . (
x1,
x2,
x3)
= [:(M . (x2,x3)),(M . (x1,x2)):] )
by ALTCAT_1:def 4, MULTOP_1:def 1;
A6:
{|M|} . ijk = {|M|} . (
x1,
x2,
x3)
by A4, MULTOP_1:def 1;
assume A7:
x in {|M,M|} . ijk
;
ex y being object st
( y in {|M|} . ijk & S1[y,x,ijk] )
then
x `1 in M . (
x2,
x3)
by A4, A5, MCART_1:10;
then
x `1 in MSAlg_morph (
S,
A,
x2,
x3)
by A1;
then consider M2,
N2 being
strict feasible MSAlgebra over
S,
g being
ManySortedFunction of
M2,
N2 such that A8:
M2 = x2
and A9:
N2 = x3
and A10:
g = x `1
and A11:
( the
Sorts of
M2 is_transformable_to the
Sorts of
N2 &
g is_homomorphism M2,
N2 )
by Def3;
x `2 in M . (
x1,
x2)
by A4, A7, A5, MCART_1:10;
then
x `2 in MSAlg_morph (
S,
A,
x1,
x2)
by A1;
then consider M1,
N1 being
strict feasible MSAlgebra over
S,
f being
ManySortedFunction of
M1,
N1 such that A12:
M1 = x1
and A13:
N1 = x2
and A14:
f = x `2
and A15:
( the
Sorts of
M1 is_transformable_to the
Sorts of
N1 &
f is_homomorphism M1,
N1 )
by Def3;
take y =
g ** f;
( y in {|M|} . ijk & S1[y,x,ijk] )
reconsider f =
f as
ManySortedFunction of
M1,
M2 by A8, A13;
( the
Sorts of
M1 is_transformable_to the
Sorts of
N2 & ex
fg being
ManySortedFunction of
M1,
N2 st
(
fg = g ** f &
fg is_homomorphism M1,
N2 ) )
by A8, A11, A13, A15, Th5, AUTALG_1:10;
then
(
{|M|} . (
x1,
x2,
x3)
= M . (
x1,
x3) &
y in MSAlg_morph (
S,
A,
x1,
x3) )
by A9, A12, Def3, ALTCAT_1:def 3;
hence
y in {|M|} . ijk
by A1, A6;
S1[y,x,ijk]
take
x1
;
ex j, k being Element of MSAlg_set (S,A) st
( ijk = [x1,j,k] & ( for f, g being Function-yielding Function st f in M . (x1,j) & g in M . (j,k) & x = [g,f] holds
y = g ** f ) )
take
x2
;
ex k being Element of MSAlg_set (S,A) st
( ijk = [x1,x2,k] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,k) & x = [g,f] holds
y = g ** f ) )
take
x3
;
( ijk = [x1,x2,x3] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds
y = g ** f ) )
thus
ijk = [x1,x2,x3]
by A4;
for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds
y = g ** f
let F,
G be
Function-yielding Function;
( F in M . (x1,x2) & G in M . (x2,x3) & x = [G,F] implies y = G ** F )
assume that
F in M . (
x1,
x2)
and
G in M . (
x2,
x3)
and A16:
x = [G,F]
;
y = G ** F
thus
y = G ** F
by A10, A14, A16;
verum
end;
consider F being ManySortedFunction of {|M,M|},{|M|} such that
A17:
for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds
ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st
( f = F . ijk & ( for x being object st x in {|M,M|} . ijk holds
S1[f . x,x,ijk] ) )
from MSSUBFAM:sch 1(A2);
take EX = AltCatStr(# (MSAlg_set (S,A)),M,F #); ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) )
reconsider EX = EX as non empty AltCatStr ;
for i, j, k being Object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f
proof
let i,
j,
k be
Object of
EX;
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** flet f,
g be
Function-yielding Function;
( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . (g,f) = g ** f )
assume A18:
(
f in the
Arrows of
EX . (
i,
j) &
g in the
Arrows of
EX . (
j,
k) )
;
( the Comp of EX . (i,j,k)) . (g,f) = g ** f
set x =
[g,f];
set ijk =
[i,j,k];
[i,j,k] in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):]
by MCART_1:69;
then consider ff being
Function of
({|M,M|} . [i,j,k]),
({|M|} . [i,j,k]) such that A19:
ff = F . [i,j,k]
and A20:
for
x being
object st
x in {|M,M|} . [i,j,k] holds
S1[
ff . x,
x,
[i,j,k]]
by A17;
A21:
ff = the
Comp of
EX . (
i,
j,
k)
by A19, MULTOP_1:def 1;
(
{|M,M|} . (
i,
j,
k)
= {|M,M|} . [i,j,k] &
{|M,M|} . (
i,
j,
k)
= [:(M . (j,k)),(M . (i,j)):] )
by ALTCAT_1:def 4, MULTOP_1:def 1;
then
[g,f] in {|M,M|} . [i,j,k]
by A18, ZFMISC_1:87;
then consider I,
J,
K being
Element of
MSAlg_set (
S,
A)
such that A22:
[i,j,k] = [I,J,K]
and A23:
for
f,
g being
Function-yielding Function st
f in M . (
I,
J) &
g in M . (
J,
K) &
[g,f] = [g,f] holds
ff . [g,f] = g ** f
by A20;
A24:
K = k
by A22, XTUPLE_0:3;
(
I = i &
J = j )
by A22, XTUPLE_0:3;
hence
( the Comp of EX . (i,j,k)) . (
g,
f)
= g ** f
by A18, A23, A24, A21;
verum
end;
hence
( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of EX
for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds
( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) )
by A1; verum