let SG be non empty non void ManySortedSign ; :: thesis:
let AG be non-empty MSAlgebra over SG; :: thesis:
let C be set ; :: thesis:
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 } ; :: thesis:

A2: now :: thesis:

let A be strict non-empty finitely-generated MSSubAlgebra of AG; :: thesis:
A in MSSub AG by MSUALG_2:def 19;
hence A in C by A1; :: thesis:

end;

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; :: thesis:
assume A3: for c being object st c in C holds
c = F . c ; :: thesis:
reconsider FF = F as MSAlgebra-Family of CC,SG ;
set pr = product FF;
defpred S₁[ 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 & S₁[i,e] ) ) from PBOOLE:sch 2();
SOR is MSSubset of (product FF)

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis:
assume A5: i in the carrier of SG ; :: thesis:
let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in SOR . i ; :: thesis:
hence e in the Sorts of (product FF) . i by A4, A5; :: thesis:

end;

then reconsider SOR = SOR as MSSubset of (product FF) ;
SOR is opers_closed

proof

let o be OperSymbol of SG; :: according to MSUALG_2:def 6 :: thesis:
set r = the_result_sort_of o;
set ar = the_arity_of o;
let q be object ; :: according to TARSKI:def 3,MSUALG_2:def 5 :: thesis:
assume A6: q in rng ((Den (o,(product FF))) | (((SOR #) * the Arity of SG) . o)) ; :: thesis:
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)) ;
S₁[ the_result_sort_of o,q]

proof

take the_result_sort_of o ; :: thesis:
take q1 ; :: thesis:

per cases ;

suppose A11: the_arity_of o = {} ; :: thesis:

end;

suppose A18: the_arity_of o <> {} ; :: thesis:

then reconsider domar = dom (the_arity_of o) as non empty finite set ;
defpred S₂[ 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 S₂[a,b]

proof

let n be Element of domar; :: thesis:
g . n in (SOR * (the_arity_of o)) . n by A19, A20, CARD_3:9;
then ( (the_arity_of o) . n in the carrier of SG & g . n in SOR . ((the_arity_of o) . n) ) by FUNCT_1:13, PARTFUN1:4;
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
A22: f = g . n and
A23: for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B by A4;
reconsider b = A as Element of MSSub AG by MSUALG_2:def 19;
take b ; :: thesis:
take f ; :: thesis:
take A ; :: thesis:
thus f = g . n by A22; :: thesis:
thus for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
f . A = f . B by A23; :: thesis:
thus b = A ; :: thesis:

end;

consider KK being Function of domar,(MSSub AG) such that
A24: for n being Element of domar holds S₂[n,KK . n] from FUNCT_2:sch 3(A21);
reconsider KK = KK as ManySortedSet of domar ;
KK is MSAlgebra-Family of domar,SG

proof

let n be object ; :: according to PRALG_2:def 5 :: thesis:
assume n in domar ; :: thesis:
then ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & KK . n = A ) by A24;
hence KK . n is MSAlgebra over SG ; :: thesis:

end;

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

proof

let n be Element of domar; :: thesis:
ex gn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( gn = g . n & ( for B being strict non-empty finitely-generated MSSubAlgebra of AG st A is MSSubAlgebra of B holds
gn . A = gn . B ) & KK . n = A ) by A24;
hence ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; :: thesis:

end;

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 ; :: thesis:
thus the_result_sort_of o = the_result_sort_of o ; :: thesis:
thus q1 = q ; :: thesis:
let B be strict non-empty finitely-generated MSSubAlgebra of AG; :: thesis:
assume A26: K is MSSubAlgebra of B ; :: thesis:
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 ; :: thesis:
assume A32: x in dom ((commute g) . iK) ; :: thesis:
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 ; :: thesis:

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 ; :: thesis:

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; :: thesis:

end;

then A40: (product FF) | SOR = MSAlgebra(# SOR,(Opers ((product FF),SOR)) #) by MSUALG_2:def 15;
defpred S₂[ 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 non-empty

proof

defpred S₃[ object ] means ex C being strict non-empty MSSubAlgebra of AG st
( $1 = C & C is finitely-generated );
let i be object ; :: according to PBOOLE:def 13 :: thesis:
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 & S₃[x] ) ) from XBOOLE_0:sch 1();
A42: ST1 c= CC

proof

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume q in ST1 ; :: thesis:
then A43: ex C being strict non-empty MSSubAlgebra of AG st
( q = C & C is finitely-generated ) by A41;
then q in MSSub AG by MSUALG_2:def 19;
hence q in CC by A1, A43; :: thesis:

end;

defpred S₄[ 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 ; :: thesis:
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 S₄[c,j]

proof

let c be object ; :: thesis:
assume c in CC ; :: thesis:
then consider C being Element of MSSub AG such that
A47: c = C and
A48: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1;
consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that
A49: R = C by A48;
consider t being object such that
A50: t in the Sorts of R . i by A44, XBOOLE_0:def 1;
take t ; :: thesis:
take R ; :: thesis:
reconsider t = t as set by TARSKI:1;
take t ; :: thesis:
thus c = R by A47, A49; :: thesis:
thus ( t in the Sorts of R . i & t = t ) by A50; :: thesis:

end;

consider f being ManySortedSet of CC such that
A51: for c being object st c in CC holds
S₄[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

proof

let a be object ; :: thesis:
assume a in dom (Carrier (FF,s)) ; :: thesis:
then A54: a in CC ;
then A55: ex U0 being MSAlgebra over SG st
( U0 = FF . a & (Carrier (FF,s)) . a = the Sorts of U0 . s ) by PRALG_2:def 9;
consider K being MSSubAlgebra of AG, t being set such that
A56: ( a = K & t in the Sorts of K . i ) and
A57: f . a = t by A51, A54;

per cases ;

suppose A58: a in ST1 ; :: thesis:

then a in dom (ST1 --> x) ;
then (f +* (ST1 --> x)) . a = (ST1 --> x) . a by FUNCT_4:13;
then A59: (f +* (ST1 --> x)) . a = x by A58, FUNCOP_1:7;
a in SuperAlgebraSet the strict non-empty finitely-generated MSSubAlgebra of AG by A41, A58;
then consider M being strict MSSubAlgebra of AG such that
A60: a = M and
A61: the strict non-empty finitely-generated MSSubAlgebra of AG is MSSubAlgebra of M by Def2;
the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG is ManySortedSubset of the Sorts of M by A61, MSUALG_2:def 9;
then the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG c= the Sorts of M by PBOOLE:def 18;
then the Sorts of the strict non-empty finitely-generated MSSubAlgebra of AG . i c= the Sorts of M . i by A44;
then x in the Sorts of M . i by A45;
hence (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A59, A60; :: thesis:

end;

suppose not a in ST1 ; :: thesis:

then (f +* (ST1 --> x)) . a = t by A52, A57, FUNCT_4:11;
hence (f +* (ST1 --> x)) . a in (Carrier (FF,s)) . a by A3, A54, A55, A56; :: thesis:

end;

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;
S₁[i,f +* (ST1 --> x)]

proof

end;

hence not SOR . i is empty by A4; :: thesis:

end;

then reconsider PS = (product FF) | SOR as strict non-empty MSSubAlgebra of product F by A40, MSUALG_1:def 3;

A65: now :: thesis:

let s be SortSymbol of SG; :: thesis:
let f be Element of (SORTS FF) . s; :: thesis:
let A be strict non-empty finitely-generated MSSubAlgebra of AG; :: thesis:
A66: 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; :: thesis:

end;

A71: now :: thesis:

let i be object ; :: thesis:
assume A72: i in the carrier of SG ; :: thesis:
let x be object ; :: thesis:
assume x in the Sorts of PS . i ; :: thesis:
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; :: thesis:
thus y in the Sorts of AG . i by A65, A73; :: thesis:
thus S₂[y,x,i] by A73, A74; :: thesis:

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
S₂[g . x,x,i] ) ) from MSSUBFAM:sch 1(A71);
take PS ; :: thesis:
take BA ; :: thesis:
thus BA is_homomorphism PS,AG :: according to MSUALG_3:def 8 :: thesis:

proof

let o be OperSymbol of SG; :: according to MSUALG_3:def 7 :: thesis:
assume Args (o,PS) <> {} ; :: thesis:
let k be Element of Args (o,PS); :: thesis:
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
S₂[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 ;

suppose A81: the_arity_of o = {} ; :: thesis:

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 ; :: thesis:

end;

suppose A86: the_arity_of o <> {} ; :: thesis:

then reconsider domar = dom (the_arity_of o) as non empty finite set ;
defpred S₃[ 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 S₃[n,b]

proof

let n be Element of domar; :: thesis:
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
S₂[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 ; :: thesis:
take f ; :: thesis:
take A ; :: thesis:
thus f = k . n by A90; :: thesis:
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; :: thesis:
thus (BA . ((the_arity_of o) . n)) . f = f . A by A88, A90, A92; :: thesis:
thus b = A ; :: thesis:

end;

consider KK being Function of domar,(MSSub AG) such that
A93: for n being Element of domar holds S₃[n,KK . n] from FUNCT_2:sch 3(A87);
reconsider KK = KK as ManySortedSet of domar ;
KK is MSAlgebra-Family of domar,SG

proof

let n be object ; :: according to PRALG_2:def 5 :: thesis:
assume n in domar ; :: thesis:
then ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( kn = k . n & ( 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) . n)) . kn = kn . A & KK . n = A ) by A93;
hence KK . n is MSAlgebra over SG ; :: thesis:

end;

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

proof

let n be Element of domar; :: thesis:
ex kn being Function ex A being strict non-empty finitely-generated MSSubAlgebra of AG st
( kn = k . n & ( 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) . n)) . kn = kn . A & KK . n = A ) by A93;
hence ex C being strict non-empty finitely-generated MSSubAlgebra of AG st C = KK . n ; :: thesis:

end;

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 ; :: thesis:
assume A103: n in dom ((commute k) . iA) ; :: thesis:
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 ;
:: thesis:

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 ; :: thesis:

end;

let i be set ; :: according to MSUALG_3:def 3 :: thesis:
assume i in the carrier of SG ; :: thesis:
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 ; :: according to XBOOLE_0:def 10 :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A111: y in the Sorts of AG . i ; :: thesis:
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 S₃[ 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 & S₃[a] ) ) from XBOOLE_0:sch 1();
set XX = aa +* (WW --> y);
A116: dom (WW --> y) = WW ;
A117: for xx being Element of CC st S₃[xx] holds
(aa +* (WW --> y)) . xx = y

proof

let xx be Element of CC; :: thesis:
assume S₃[xx] ; :: thesis:
then A118: xx in WW by A115;
hence (aa +* (WW --> y)) . xx = (WW --> y) . xx by A116, FUNCT_4:13
.= y by A118, FUNCOP_1:7 ;
:: thesis:

end;

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

proof

let x be object ; :: thesis:
assume A121: x in dom (Carrier (FF,s)) ; :: thesis:
then consider C being Element of MSSub AG such that
A122: x = C and
A123: ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = C by A1, A119;
consider R being strict non-empty finitely-generated MSSubAlgebra of AG such that
A124: R = C by A123;
A125: R in CC by A1, A124;
then A126: ( ex U0 being MSAlgebra over SG st
( U0 = FF . R & (Carrier (FF,s)) . R = the Sorts of U0 . s ) & FF . R = R ) by A3, PRALG_2:def 9;

per cases ;

suppose S₃[x] ; :: thesis:

hence (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A117, A122, A124, A125, A126; :: thesis:

end;

suppose not S₃[x] ; :: thesis:

then not x in WW by A115;
then (aa +* (WW --> y)) . x = aa . x by A116, FUNCT_4:11;
hence (aa +* (WW --> y)) . x in (Carrier (FF,s)) . x by A114, A121; :: thesis:

end;

A127: WW c= CC by A115;
set L = the non-empty finite-yielding MSSubset of AG;
A128: dom (BA . s) = the Sorts of PS . s by FUNCT_2:def 1;
set SY = {s} --> {y};
dom ( the non-empty finite-yielding MSSubset of AG +* ({s} --> {y})) = (dom the non-empty finite-yielding 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 non-empty finite-yielding 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 ;

A131: now :: thesis:

let k be set ; :: thesis:
assume that
k in the carrier of SG and
A132: k <> s ; :: thesis:
not k in dom ({s} --> {y}) by A132, TARSKI:def 1;
hence Y . k = the non-empty finite-yielding MSSubset of AG . k by FUNCT_4:11; :: thesis:

end;

Y is ManySortedSubset of the Sorts of AG

proof

let j be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis:
assume A133: j in the carrier of SG ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A134: x in Y . j ; :: thesis:

per cases ;

suppose A135: j <> s ; :: thesis:

the non-empty finite-yielding MSSubset of AG c= the Sorts of AG by PBOOLE:def 18;
then A136: the non-empty finite-yielding MSSubset of AG . j c= the Sorts of AG . j by A133;
x in the non-empty finite-yielding MSSubset of AG . j by A131, A133, A134, A135;
hence x in the Sorts of AG . j by A136; :: thesis:

end;

suppose j = s ; :: thesis:

hence x in the Sorts of AG . j by A111, A130, A134, TARSKI:def 1; :: thesis:

end;

then reconsider Y = Y as MSSubset of AG ;
Y is non-empty

proof

let j be object ; :: according to PBOOLE:def 13 :: thesis:
assume A137: j in the carrier of SG ; :: thesis:

per cases ;

suppose j <> s ; :: thesis:

then Y . j = the non-empty finite-yielding MSSubset of AG . j by A131, A137;
hence not Y . j is empty by A137; :: thesis:

end;

suppose j = s ; :: thesis:

hence not Y . j is empty by A130; :: thesis:

end;

then reconsider Y = Y as non-empty MSSubset of AG ;
Y is finite-yielding

proof

let j be object ; :: according to FINSET_1:def 5 :: thesis:
assume A138: j in the carrier of SG ; :: thesis:

per cases ;

suppose j <> s ; :: thesis:

then Y . j = the non-empty finite-yielding MSSubset of AG . j by A131, A138;
hence Y . j is finite ; :: thesis:

end;

suppose j = s ; :: thesis:

hence Y . j is finite by A130; :: thesis:

end;

then reconsider Y = Y as non-empty finite-yielding 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
S₂[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;
S₁[s,XX]

proof

take s ; :: thesis:
take XX ; :: thesis:
take TT = GenMSAlg Y; :: thesis:
thus s = s ; :: thesis:
thus XX = XX ; :: thesis:
let B be strict non-empty finitely-generated MSSubAlgebra of AG; :: thesis:
assume TT is MSSubAlgebra of B ; :: thesis:
then the Sorts of TT is ManySortedSubset of the Sorts of B by MSUALG_2:def 9;
then the Sorts of TT c= the Sorts of B by PBOOLE:def 18;
then A144: the Sorts of TT . s c= the Sorts of B . s ;
A145: B in CC by A2;
TT in CC by A2;
hence XX . TT = y by A139, A142, A117
.= XX . B by A143, A117, A145, A144 ;
:: thesis:

end;

then A146: XX in SOR . s by A4;
then S₂[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; :: thesis: