let SG be non empty non void ManySortedSign ; for AG being non-empty MSAlgebra over SG
for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds
for F being MSAlgebra-Family of C,SG st ( for c being object st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
let AG be non-empty MSAlgebra over SG; for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds
for F being MSAlgebra-Family of C,SG st ( for c being object st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
let C be set ; ( C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } implies for F being MSAlgebra-Family of C,SG st ( for c being object st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG )
assume A1:
C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A }
; for F being MSAlgebra-Family of C,SG st ( for c being object st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
then reconsider CC = C as non empty set ;
set T = the strict non-empty finitely-generated MSSubAlgebra of AG;
set I = the carrier of SG;
let F be MSAlgebra-Family of C,SG; ( ( for c being object st c in C holds
c = F . c ) implies ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG )
assume A3:
for c being object st c in C holds
c = F . c
; ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
reconsider FF = F as MSAlgebra-Family of CC,SG ;
set pr = product FF;
defpred S1[ object , object ] means ex t being SortSymbol of SG ex f being Element of (SORTS FF) . t ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( t = $1 & f = $2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) );
consider SOR being ManySortedSet of the carrier of SG such that
A4:
for i being object st i in the carrier of SG holds
for e being object holds
( e in SOR . i iff ( e in (SORTS FF) . i & S1[i,e] ) )
from PBOOLE:sch 2();
SOR is MSSubset of (product FF)
then reconsider SOR = SOR as MSSubset of (product FF) ;
SOR is opers_closed
proof
let o be
OperSymbol of
SG;
MSUALG_2:def 6 SOR is_closed_on o
set r =
the_result_sort_of o;
set ar =
the_arity_of o;
let q be
object ;
TARSKI:def 3,
MSUALG_2:def 5 ( not q in proj2 ((Den (o,(product FF))) | (( the Arity of SG * (SOR #)) . o)) or q in ( the ResultSort of SG * SOR) . o )
assume A6:
q in rng ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o))
;
q in ( the ResultSort of SG * SOR) . o
reconsider q1 =
q as
Element of
(SORTS FF) . (the_result_sort_of o) by A6, PRALG_2:3;
consider g being
object such that A7:
g in dom ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o))
and A8:
q = ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) . g
by A6, FUNCT_1:def 3;
A9:
q = (Den (o,(product FF))) . g
by A7, A8, FUNCT_1:47;
A10:
g in ((SOR #) * the Arity of SG) . o
by A7;
g in dom (Den (o,(product FF)))
by A7, RELAT_1:57;
then reconsider g =
g as
Element of
Args (
o,
(product FF)) ;
S1[
the_result_sort_of o,
q]
proof
take
the_result_sort_of o
;
ex f being Element of (SORTS FF) . (the_result_sort_of o) ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & f = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) )
take
q1
;
ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )
per cases
( the_arity_of o = {} or the_arity_of o <> {} )
;
suppose A11:
the_arity_of o = {}
;
ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )set A = the
strict non-empty finitely-generated MSSubAlgebra of
AG;
Args (
o, the
strict non-empty finitely-generated MSSubAlgebra of
AG)
= {{}}
by A11, PRALG_2:4;
then A12:
{} in Args (
o, the
strict non-empty finitely-generated MSSubAlgebra of
AG)
by TARSKI:def 1;
take
the
strict non-empty finitely-generated MSSubAlgebra of
AG
;
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) )thus
the_result_sort_of o = the_result_sort_of o
;
( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B ) )thus
q1 = q
;
for B being strict non-empty finitely-generated MSSubAlgebra of AG st the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B holds
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . Blet B be
strict non-empty finitely-generated MSSubAlgebra of
AG;
( the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of B implies q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B )assume
the
strict non-empty finitely-generated MSSubAlgebra of
AG is
MSSubAlgebra of
B
;
q1 . the strict non-empty finitely-generated MSSubAlgebra of AG = q1 . B
Args (
o,
B)
= {{}}
by A11, PRALG_2:4;
then A13:
{} in Args (
o,
B)
by TARSKI:def 1;
B in MSSub AG
by MSUALG_2:def 19;
then A14:
B in CC
by A1;
the
strict non-empty finitely-generated MSSubAlgebra of
AG in MSSub AG
by MSUALG_2:def 19;
then
the
strict non-empty finitely-generated MSSubAlgebra of
AG in CC
by A1;
then reconsider iA = the
strict non-empty finitely-generated MSSubAlgebra of
AG,
iB =
B as
Element of
CC by A14;
A15:
iA = FF . iA
by A3;
A16:
iB = FF . iB
by A3;
Args (
o,
(product FF))
= {{}}
by A11, PRALG_2:4;
then A17:
g = {}
by TARSKI:def 1;
hence q1 . the
strict non-empty finitely-generated MSSubAlgebra of
AG =
(const (o,(product FF))) . iA
by A9, PRALG_3:def 1
.=
const (
o,
(FF . iA))
by A11, PRALG_3:9
.=
(Den (o,(FF . iA))) . {}
by PRALG_3:def 1
.=
(Den (o,AG)) . {}
by A15, A12, Th19
.=
(Den (o,(FF . iB))) . {}
by A16, A13, Th19
.=
const (
o,
(FF . iB))
by PRALG_3:def 1
.=
(const (o,(product FF))) . iB
by A11, PRALG_3:9
.=
q1 . B
by A9, A17, PRALG_3:def 1
;
verum end; suppose A18:
the_arity_of o <> {}
;
ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
q1 . A = q1 . B ) )then reconsider domar =
dom (the_arity_of o) as non
empty finite set ;
defpred S2[
set ,
set ]
means ex
gn being
Function ex
A being
strict non-empty finitely-generated MSSubAlgebra of
AG st
(
gn = g . $1 & ( for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
gn . A = gn . B ) & $2
= A );
g in (SOR #) . ( the Arity of SG . o)
by A10, FUNCT_2:15;
then A19:
g in product (SOR * (the_arity_of o))
by FINSEQ_2:def 5;
then A20:
dom (SOR * (the_arity_of o)) =
dom g
by CARD_3:9
.=
domar
by MSUALG_3:6
;
A21:
for
a being
Element of
domar ex
b being
Element of
MSSub AG st
S2[
a,
b]
consider KK being
Function of
domar,
(MSSub AG) such that A24:
for
n being
Element of
domar holds
S2[
n,
KK . n]
from FUNCT_2:sch 3(A21);
reconsider KK =
KK as
ManySortedSet of
domar ;
KK is
MSAlgebra-Family of
domar,
SG
then reconsider KK =
KK as
MSAlgebra-Family of
domar,
SG ;
for
n being
Element of
domar ex
C being
strict non-empty finitely-generated MSSubAlgebra of
AG st
C = KK . n
then consider K being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A25:
for
n being
Element of
domar holds
KK . n is
MSSubAlgebra of
K
by Th25;
take
K
;
( the_result_sort_of o = the_result_sort_of o & q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . B ) )thus
the_result_sort_of o = the_result_sort_of o
;
( q1 = q & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . B ) )thus
q1 = q
;
for B being strict non-empty finitely-generated MSSubAlgebra of AG st K is MSSubAlgebra of B holds
q1 . K = q1 . Blet B be
strict non-empty finitely-generated MSSubAlgebra of
AG;
( K is MSSubAlgebra of B implies q1 . K = q1 . B )assume A26:
K is
MSSubAlgebra of
B
;
q1 . K = q1 . B
K in MSSub AG
by MSUALG_2:def 19;
then A27:
K in CC
by A1;
B in MSSub AG
by MSUALG_2:def 19;
then
B in CC
by A1;
then reconsider iB =
B,
iK =
K as
Element of
CC by A27;
A28:
g in Funcs (
(dom (the_arity_of o)),
(Funcs (CC,(union { ( the Sorts of (FF . i) . s) where i is Element of CC, s is Element of the carrier of SG : verum } ))))
by PRALG_3:14;
then A29:
dom ((commute g) . iB) = domar
by Th3;
A30:
dom ((commute g) . iK) = domar
by A28, Th3;
A31:
for
n being
object st
n in dom ((commute g) . iK) holds
((commute g) . iB) . n = ((commute g) . iK) . n
proof
let x be
object ;
( x in dom ((commute g) . iK) implies ((commute g) . iB) . x = ((commute g) . iK) . x )
assume A32:
x in dom ((commute g) . iK)
;
((commute g) . iB) . x = ((commute g) . iK) . x
then consider gn being
Function,
A being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A33:
gn = g . x
and A34:
( ( for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
gn . A = gn . B ) &
KK . x = A )
by A24, A30;
A35:
KK . x is
MSSubAlgebra of
K
by A25, A30, A32;
thus ((commute g) . iB) . x =
gn . iB
by A30, A32, A33, PRALG_3:21
.=
gn . A
by A26, A34, A35, MSUALG_2:6
.=
gn . iK
by A25, A30, A32, A34
.=
((commute g) . iK) . x
by A30, A32, A33, PRALG_3:21
;
verum
end; A36:
iK = FF . iK
by A3;
A37:
(commute g) . iK is
Element of
Args (
o,
(FF . iK))
by A18, PRALG_3:20;
A38:
(commute g) . iB is
Element of
Args (
o,
(FF . iB))
by A18, PRALG_3:20;
A39:
iB = FF . iB
by A3;
thus q1 . K =
(Den (o,(FF . iK))) . ((commute g) . iK)
by A9, A18, PRALG_3:22
.=
(Den (o,AG)) . ((commute g) . iK)
by A36, A37, Th19
.=
(Den (o,AG)) . ((commute g) . iB)
by A28, A29, A31, Th3, FUNCT_1:2
.=
(Den (o,(FF . iB))) . ((commute g) . iB)
by A39, A38, Th19
.=
q1 . B
by A9, A18, PRALG_3:22
;
verum end; end;
end;
then
q in SOR . (the_result_sort_of o)
by A4;
hence
q in ( the ResultSort of SG * SOR) . o
by FUNCT_2:15;
verum
end;
then A40:
(product FF) | SOR = MSAlgebra(# SOR,(Opers ((product FF),SOR)) #)
by MSUALG_2:def 15;
defpred S2[ object , object , object ] means ex s being SortSymbol of SG ex f being Element of (SORTS FF) . s ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( s = $3 & f = $2 & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & $1 = f . A );
SOR is V2()
proof
defpred S3[
object ]
means ex
C being
strict non-empty MSSubAlgebra of
AG st
( $1
= C &
C is
finitely-generated );
let i be
object ;
PBOOLE:def 13 ( not i in the carrier of SG or not SOR . i is empty )
consider ST1 being
set such that A41:
for
x being
object holds
(
x in ST1 iff (
x in SuperAlgebraSet the
strict non-empty finitely-generated MSSubAlgebra of
AG &
S3[
x] ) )
from XBOOLE_0:sch 1();
A42:
ST1 c= CC
defpred S4[
object ,
object ]
means ex
K being
MSSubAlgebra of
AG ex
t being
set st
( $1
= K &
t in the
Sorts of
K . i & $2
= t );
assume A44:
i in the
carrier of
SG
;
not SOR . i is empty
then consider x being
object such that A45:
x in the
Sorts of the
strict non-empty finitely-generated MSSubAlgebra of
AG . i
by XBOOLE_0:def 1;
reconsider s =
i as
SortSymbol of
SG by A44;
A46:
for
c being
object st
c in CC holds
ex
j being
object st
S4[
c,
j]
consider f being
ManySortedSet of
CC such that A51:
for
c being
object st
c in CC holds
S4[
c,
f . c]
from PBOOLE:sch 3(A46);
set g =
f +* (ST1 --> x);
A52:
dom (ST1 --> x) = ST1
;
A53:
for
a being
object st
a in dom (Carrier (FF,s)) holds
(f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a
dom (f +* (ST1 --> x)) =
(dom f) \/ (dom (ST1 --> x))
by FUNCT_4:def 1
.=
CC \/ (dom (ST1 --> x))
by PARTFUN1:def 2
.=
CC \/ ST1
.=
CC
by A42, XBOOLE_1:12
.=
dom (Carrier (FF,s))
by PARTFUN1:def 2
;
then A62:
f +* (ST1 --> x) in product (Carrier (FF,s))
by A53, CARD_3:9;
S1[
i,
f +* (ST1 --> x)]
hence
not
SOR . i is
empty
by A4;
verum
end;
then reconsider PS = (product FF) | SOR as strict non-empty MSSubAlgebra of product F by A40, MSUALG_1:def 3;
A65:
now for s being SortSymbol of SG
for f being Element of (SORTS FF) . s
for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . slet s be
SortSymbol of
SG;
for f being Element of (SORTS FF) . s
for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . slet f be
Element of
(SORTS FF) . s;
for A being strict non-empty finitely-generated MSSubAlgebra of AG holds f . A in the Sorts of AG . slet A be
strict non-empty finitely-generated MSSubAlgebra of
AG;
f . A in the Sorts of AG . sA66:
dom (Carrier (FF,s)) = CC
by PARTFUN1:def 2;
A in MSSub AG
by MSUALG_2:def 19;
then A67:
A in dom (Carrier (FF,s))
by A1, A66;
then consider U0 being
MSAlgebra over
SG such that A68:
U0 = FF . A
and A69:
(Carrier (FF,s)) . A = the
Sorts of
U0 . s
by PRALG_2:def 9;
(SORTS FF) . s = product (Carrier (FF,s))
by PRALG_2:def 10;
then A70:
f . A in (Carrier (FF,s)) . A
by A67, CARD_3:9;
FF . A = A
by A3, A67;
then
the
Sorts of
U0 is
ManySortedSubset of the
Sorts of
AG
by A68, MSUALG_2:def 9;
then
the
Sorts of
U0 c= the
Sorts of
AG
by PBOOLE:def 18;
then
the
Sorts of
U0 . s c= the
Sorts of
AG . s
;
hence
f . A in the
Sorts of
AG . s
by A69, A70;
verum end;
A71:
now for i being object st i in the carrier of SG holds
for x being object st x in the Sorts of PS . i holds
ex y being object st
( y in the Sorts of AG . i & S2[y,x,i] )let i be
object ;
( i in the carrier of SG implies for x being object st x in the Sorts of PS . i holds
ex y being object st
( y in the Sorts of AG . i & S2[y,x,i] ) )assume A72:
i in the
carrier of
SG
;
for x being object st x in the Sorts of PS . i holds
ex y being object st
( y in the Sorts of AG . i & S2[y,x,i] )let x be
object ;
( x in the Sorts of PS . i implies ex y being object st
( y in the Sorts of AG . i & S2[y,x,i] ) )assume
x in the
Sorts of
PS . i
;
ex y being object st
( y in the Sorts of AG . i & S2[y,x,i] )then consider s being
SortSymbol of
SG,
f being
Element of
(SORTS FF) . s,
A being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A73:
s = i
and A74:
(
f = x & ( for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
f . A = f . B ) )
by A4, A40, A72;
reconsider y =
f . A as
object ;
take y =
y;
( y in the Sorts of AG . i & S2[y,x,i] )thus
y in the
Sorts of
AG . i
by A65, A73;
S2[y,x,i]thus
S2[
y,
x,
i]
by A73, A74;
verum end;
consider BA being ManySortedFunction of PS,AG such that
A75:
for i being object st i in the carrier of SG holds
ex g being Function of ( the Sorts of PS . i),( the Sorts of AG . i) st
( g = BA . i & ( for x being object st x in the Sorts of PS . i holds
S2[g . x,x,i] ) )
from MSSUBFAM:sch 1(A71);
take
PS
; ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG
take
BA
; BA is_epimorphism PS,AG
thus
BA is_homomorphism PS,AG
MSUALG_3:def 8 BA is "onto" proof
let o be
OperSymbol of
SG;
MSUALG_3:def 7 ( Args (o,PS) = {} or for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1) )
assume
Args (
o,
PS)
<> {}
;
for b1 being Element of Args (o,PS) holds (BA . (the_result_sort_of o)) . ((Den (o,PS)) . b1) = (Den (o,AG)) . (BA # b1)
let k be
Element of
Args (
o,
PS);
(BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)
set r =
the_result_sort_of o;
set ar =
the_arity_of o;
consider g being
Function of
( the Sorts of PS . (the_result_sort_of o)),
( the Sorts of AG . (the_result_sort_of o)) such that A76:
g = BA . (the_result_sort_of o)
and A77:
for
k being
object st
k in the
Sorts of
PS . (the_result_sort_of o) holds
S2[
g . k,
k,
the_result_sort_of o]
by A75;
consider s being
SortSymbol of
SG,
f being
Element of
(SORTS FF) . s,
A being
strict non-empty finitely-generated MSSubAlgebra of
AG such that
s = the_result_sort_of o
and A78:
f = (Den (o,PS)) . k
and A79:
for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
f . A = f . B
and A80:
g . ((Den (o,PS)) . k) = f . A
by A77, MSUALG_9:18;
per cases
( the_arity_of o = {} or the_arity_of o <> {} )
;
suppose A81:
the_arity_of o = {}
;
(BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)
A in MSSub AG
by MSUALG_2:def 19;
then
A in CC
by A1;
then reconsider iA =
A as
Element of
CC ;
reconsider ff1 =
(Den (o,(product FF))) . k as
Function by Th20;
A82:
(Den (o,(product FF))) . {} = const (
o,
(product FF))
by PRALG_3:def 1;
Args (
o,
A)
= {{}}
by A81, PRALG_2:4;
then A83:
{} in Args (
o,
A)
by TARSKI:def 1;
A84:
Args (
o,
PS)
= {{}}
by A81, PRALG_2:4;
then A85:
k = {}
by TARSKI:def 1;
thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) =
ff1 . A
by A76, A78, A80, Th19
.=
(const (o,(product FF))) . iA
by A84, A82, TARSKI:def 1
.=
const (
o,
(FF . iA))
by A81, PRALG_3:9
.=
(Den (o,(FF . iA))) . {}
by PRALG_3:def 1
.=
(Den (o,A)) . {}
by A3
.=
(Den (o,AG)) . {}
by A83, Th19
.=
(Den (o,AG)) . (BA # k)
by A81, A85, PRALG_3:11
;
verum end; suppose A86:
the_arity_of o <> {}
;
(BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) = (Den (o,AG)) . (BA # k)then reconsider domar =
dom (the_arity_of o) as non
empty finite set ;
defpred S3[
set ,
set ]
means ex
kn being
Function ex
A being
strict non-empty finitely-generated MSSubAlgebra of
AG st
(
kn = k . $1 & ( for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
kn . A = kn . B ) &
(BA . ((the_arity_of o) . $1)) . kn = kn . A & $2
= A );
A87:
for
n being
Element of
domar ex
b being
Element of
MSSub AG st
S3[
n,
b]
proof
let n be
Element of
domar;
ex b being Element of MSSub AG st S3[n,b]
consider g being
Function of
( the Sorts of PS . ((the_arity_of o) . n)),
( the Sorts of AG . ((the_arity_of o) . n)) such that A88:
g = BA . ((the_arity_of o) . n)
and A89:
for
x being
object st
x in the
Sorts of
PS . ((the_arity_of o) . n) holds
S2[
g . x,
x,
(the_arity_of o) . n]
by A75, PARTFUN1:4;
k . n in the
Sorts of
PS . ((the_arity_of o) /. n)
by MSUALG_6:2;
then
k . n in the
Sorts of
PS . ((the_arity_of o) . n)
by PARTFUN1:def 6;
then consider s being
SortSymbol of
SG,
f being
Element of
(SORTS FF) . s,
A being
strict non-empty finitely-generated MSSubAlgebra of
AG such that
s = (the_arity_of o) . n
and A90:
f = k . n
and A91:
for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
f . A = f . B
and A92:
g . (k . n) = f . A
by A89;
reconsider b =
A as
Element of
MSSub AG by MSUALG_2:def 19;
take
b
;
S3[n,b]
take
f
;
ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
take
A
;
( f = k . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus
f = k . n
by A90;
( ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus
for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
A is
MSSubAlgebra of
B holds
f . A = f . B
by A91;
( (BA . ((the_arity_of o) . n)) . f = f . A & b = A )
thus
(BA . ((the_arity_of o) . n)) . f = f . A
by A88, A90, A92;
b = A
thus
b = A
;
verum
end; consider KK being
Function of
domar,
(MSSub AG) such that A93:
for
n being
Element of
domar holds
S3[
n,
KK . n]
from FUNCT_2:sch 3(A87);
reconsider KK =
KK as
ManySortedSet of
domar ;
KK is
MSAlgebra-Family of
domar,
SG
then reconsider KK =
KK as
MSAlgebra-Family of
domar,
SG ;
for
n being
Element of
domar ex
C being
strict non-empty finitely-generated MSSubAlgebra of
AG st
C = KK . n
then consider K being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A94:
for
n being
Element of
domar holds
KK . n is
MSSubAlgebra of
K
by Th25;
consider MAX being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A95:
A is
MSSubAlgebra of
MAX
and A96:
K is
MSSubAlgebra of
MAX
by Th26;
MAX in MSSub AG
by MSUALG_2:def 19;
then
MAX in CC
by A1;
then reconsider iA =
MAX as
Element of
CC ;
A97:
k in Args (
o,
(product FF))
by Th18;
then A98:
(commute k) . iA is
Element of
Args (
o,
(FF . iA))
by A86, PRALG_3:20;
then
(commute k) . iA in Args (
o,
(FF . iA))
;
then A99:
(commute k) . iA in Args (
o,
MAX)
by A3;
A100:
k in Funcs (
(dom (the_arity_of o)),
(Funcs (CC,(union { ( the Sorts of (FF . i) . m) where i is Element of CC, m is Element of the carrier of SG : verum } ))))
by A97, PRALG_3:14;
then A101:
dom ((commute k) . iA) = domar
by Th3;
A102:
for
n being
object st
n in dom ((commute k) . iA) holds
(BA # k) . n = ((commute k) . iA) . n
proof
set fs =
(commute k) . iA;
reconsider fs =
(commute k) . iA as
Element of
Args (
o,
MAX)
by A3, A98;
let n be
object ;
( n in dom ((commute k) . iA) implies (BA # k) . n = ((commute k) . iA) . n )
assume A103:
n in dom ((commute k) . iA)
;
(BA # k) . n = ((commute k) . iA) . n
then reconsider arn =
(the_arity_of o) . n as
SortSymbol of
SG by A101, PARTFUN1:4;
n in Seg (len fs)
by A103, FINSEQ_1:def 3;
then reconsider n9 =
n as
Nat ;
consider kn being
Function,
Ki being
strict non-empty finitely-generated MSSubAlgebra of
AG such that A104:
kn = k . n
and A105:
for
B being
strict non-empty finitely-generated MSSubAlgebra of
AG st
Ki is
MSSubAlgebra of
B holds
kn . Ki = kn . B
and A106:
(BA . arn) . kn = kn . Ki
and A107:
KK . n = Ki
by A93, A101, A103;
A108:
Ki is
MSSubAlgebra of
K
by A94, A101, A103, A107;
dom k = domar
by A100, FUNCT_2:92;
hence (BA # k) . n =
(BA . ((the_arity_of o) /. n9)) . (k . n)
by A101, A103, MSUALG_3:def 6
.=
kn . (KK . n)
by A101, A103, A104, A106, A107, PARTFUN1:def 6
.=
kn . iA
by A96, A105, A107, A108, MSUALG_2:6
.=
((commute k) . iA) . n
by A97, A101, A103, A104, PRALG_3:21
;
verum
end; reconsider ff1 =
(Den (o,(product FF))) . k as
Function by Th20;
A109:
dom (BA # k) = domar
by MSUALG_6:2;
thus (BA . (the_result_sort_of o)) . ((Den (o,PS)) . k) =
f . MAX
by A76, A79, A80, A95
.=
ff1 . MAX
by A78, Th19
.=
(Den (o,(FF . iA))) . ((commute k) . iA)
by A86, A97, PRALG_3:22
.=
(Den (o,MAX)) . ((commute k) . iA)
by A3
.=
(Den (o,AG)) . ((commute k) . iA)
by A99, Th19
.=
(Den (o,AG)) . (BA # k)
by A100, A109, A102, Th3, FUNCT_1:2
;
verum end; end;
end;
let i be set ; MSUALG_3:def 3 ( not i in the carrier of SG or proj2 (BA . i) = the Sorts of AG . i )
assume
i in the carrier of SG
; proj2 (BA . i) = the Sorts of AG . i
then reconsider s = i as SortSymbol of SG ;
consider ff being object such that
A110:
ff in the Sorts of PS . s
by XBOOLE_0:def 1;
rng (BA . s) c= the Sorts of AG . s
;
hence
rng (BA . i) c= the Sorts of AG . i
; XBOOLE_0:def 10 the Sorts of AG . i c= proj2 (BA . i)
let y be object ; TARSKI:def 3 ( not y in the Sorts of AG . i or y in proj2 (BA . i) )
assume A111:
y in the Sorts of AG . i
; y in proj2 (BA . i)
A112:
(SORTS FF) . s = product (Carrier (FF,s))
by PRALG_2:def 10;
then
ff in product (Carrier (FF,s))
by A4, A40, A110;
then consider aa being Function such that
ff = aa
and
A113:
dom aa = dom (Carrier (FF,s))
and
A114:
for x being object st x in dom (Carrier (FF,s)) holds
aa . x in (Carrier (FF,s)) . x
by CARD_3:def 5;
defpred S3[ object ] means ex Axx being MSSubAlgebra of AG st
( Axx = $1 & y in the Sorts of Axx . s );
consider WW being set such that
A115:
for a being object holds
( a in WW iff ( a in CC & S3[a] ) )
from XBOOLE_0:sch 1();
set XX = aa +* (WW --> y);
A116:
dom (WW --> y) = WW
;
A117:
for xx being Element of CC st S3[xx] holds
(aa +* (WW --> y)) . xx = y
A119:
dom (Carrier (FF,s)) = CC
by PARTFUN1:def 2;
A120:
for x being object st x in dom (Carrier (FF,s)) holds
(aa +* (WW --> y)) . x in (Carrier (FF,s)) . x
A127:
WW c= CC
by A115;
set L = the V2() V32() MSSubset of AG;
A128:
dom (BA . s) = the Sorts of PS . s
by FUNCT_2:def 1;
set SY = {s} --> {y};
dom ( the V2() V32() MSSubset of AG +* ({s} --> {y})) =
(dom the V2() V32() MSSubset of AG) \/ (dom ({s} --> {y}))
by FUNCT_4:def 1
.=
the carrier of SG \/ (dom ({s} --> {y}))
by PARTFUN1:def 2
.=
the carrier of SG \/ {s}
.=
the carrier of SG
by ZFMISC_1:40
;
then reconsider Y = the V2() V32() MSSubset of AG +* ({s} --> {y}) as ManySortedSet of the carrier of SG by PARTFUN1:def 2, RELAT_1:def 18;
A129:
s in {s}
by TARSKI:def 1;
dom ({s} --> {y}) = {s}
;
then A130: Y . s =
({s} --> {y}) . s
by A129, FUNCT_4:13
.=
{y}
by A129, FUNCOP_1:7
;
Y is ManySortedSubset of the Sorts of AG
then reconsider Y = Y as MSSubset of AG ;
Y is V2()
then reconsider Y = Y as V2() MSSubset of AG ;
Y is V32()
then reconsider Y = Y as V2() V32() MSSubset of AG ;
Y is MSSubset of (GenMSAlg Y)
by MSUALG_2:def 17;
then
Y c= the Sorts of (GenMSAlg Y)
by PBOOLE:def 18;
then A139:
Y . s c= the Sorts of (GenMSAlg Y) . s
;
dom (aa +* (WW --> y)) =
(dom aa) \/ (dom (WW --> y))
by FUNCT_4:def 1
.=
CC \/ (dom (WW --> y))
by A113, PARTFUN1:def 2
.=
CC \/ WW
.=
CC
by A127, XBOOLE_1:12
;
then reconsider XX = aa +* (WW --> y) as Element of (SORTS FF) . s by A112, A119, A120, CARD_3:9;
consider h being Function of ( the Sorts of PS . s),( the Sorts of AG . s) such that
A140:
h = BA . s
and
A141:
for x being object st x in the Sorts of PS . s holds
S2[h . x,x,s]
by A75;
A142:
y in Y . s
by A130, TARSKI:def 1;
then A143:
y in the Sorts of (GenMSAlg Y) . s
by A139;
S1[s,XX]
then A146:
XX in SOR . s
by A4;
then
S2[h . XX,XX,s]
by A40, A141;
then consider t being SortSymbol of SG, f being Element of (SORTS FF) . s, A being strict non-empty finitely-generated MSSubAlgebra of AG such that
s = t
and
A147:
( f = XX & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B ) & h . XX = f . A )
;
consider MAX being strict non-empty finitely-generated MSSubAlgebra of AG such that
A148:
A is MSSubAlgebra of MAX
and
A149:
GenMSAlg Y is MSSubAlgebra of MAX
by Th26;
A150:
MAX in CC
by A2;
the Sorts of (GenMSAlg Y) is ManySortedSubset of the Sorts of MAX
by A149, MSUALG_2:def 9;
then
the Sorts of (GenMSAlg Y) c= the Sorts of MAX
by PBOOLE:def 18;
then A151:
the Sorts of (GenMSAlg Y) . s c= the Sorts of MAX . s
;
h . XX =
XX . MAX
by A147, A148
.=
y
by A143, A117, A151, A150
;
hence
y in proj2 (BA . i)
by A40, A128, A140, A146, FUNCT_1:def 3; verum