let S be non empty non void ManySortedSign ; :: thesis: for I being non empty finite set
for A being non-empty MSAlgebra over S
for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds
ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B
let I be non empty finite set ; :: thesis: for A being non-empty MSAlgebra over S
for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds
ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B
let A be non-empty MSAlgebra over S; :: thesis: for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds
ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B
let F be MSAlgebra-Family of I,S; :: thesis: ( ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) implies ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B )
assume A1: for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ; :: thesis: ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B
set Z = { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D ) } ;
set J = the carrier of S;
set m = the Element of I;
consider W being strict non-empty finitely-generated MSSubAlgebra of A such that
A2: W = F . the Element of I by A1;
W is Element of MSSub A by MSUALG_2:def 19;
then W in { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D ) } by A2;
then reconsider Z = { C where C is Element of MSSub A : ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D ) } as non empty set ;
defpred S₁[ set , set ] means ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( $1 = Q & $2 = G & G is non-empty & G is finite-yielding );
A3: for a being Element of Z ex b being Element of Bool the Sorts of A st S₁[a,b]

proof

let a be Element of Z; :: thesis: ex b being Element of Bool the Sorts of A st S₁[a,b]
a in Z ;
then consider C being Element of MSSub A such that
A4: a = C and
A5: ex i being Element of I ex D being strict non-empty finitely-generated MSSubAlgebra of A st
( C = F . i & C = D ) ;
consider i being Element of I, D being strict non-empty finitely-generated MSSubAlgebra of A such that
C = F . i and
A6: C = D by A5;
consider G being GeneratorSet of D such that
A7: G is finite-yielding by MSAFREE2:def 10;
consider S being non-empty finite-yielding ManySortedSubset of the Sorts of D such that
A8: G c= S by A7, MSUALG_9:7;
the Sorts of D is MSSubset of A by MSUALG_2:def 9;
then ( S c= the Sorts of D & the Sorts of D c= the Sorts of A ) by PBOOLE:def 18;
then S c= the Sorts of A by PBOOLE:13;
then S is ManySortedSubset of the Sorts of A by PBOOLE:def 18;
then reconsider b = S as Element of Bool the Sorts of A by CLOSURE2:def 1;
reconsider S = S as GeneratorSet of D by A8, MSSCYC_1:21;
take b ; :: thesis: S₁[a,b]
take D ; :: thesis: ex G being GeneratorSet of D st
( a = D & b = G & G is non-empty & G is finite-yielding )
take S ; :: thesis: ( a = D & b = S & S is non-empty & S is finite-yielding )
thus a = D by A4, A6; :: thesis: ( b = S & S is non-empty & S is finite-yielding )
thus ( b = S & S is non-empty & S is finite-yielding ) ; :: thesis: verum

end;

consider f being Function of Z,(Bool the Sorts of A) such that
A9: for B being Element of Z holds S₁[B,f . B] from FUNCT_2:sch 3(A3);
deffunc H₁( object ) -> set = union { a where a is Element of bool ( the Sorts of A . $1) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . $1 ) } ;
consider SOR being ManySortedSet of the carrier of S such that
A10: for j being object st j in the carrier of S holds
SOR . j = H₁(j) from PBOOLE:sch 4();
SOR is ManySortedSubset of the Sorts of A

proof

let j be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not j in the carrier of S or SOR . j c= the Sorts of A . j )
assume A11: j in the carrier of S ; :: thesis: SOR . j c= the Sorts of A . j
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in SOR . j or q in the Sorts of A . j )
set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
assume q in SOR . j ; :: thesis: q in the Sorts of A . j
then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } by A10, A11;
then consider w being set such that
A12: q in w and
A13: w in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } by TARSKI:def 4;
consider a being Element of bool ( the Sorts of A . j) such that
A14: w = a and
ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) by A13;
thus q in the Sorts of A . j by A12, A14; :: thesis: verum

end;

then reconsider SOR = SOR as MSSubset of A ;
SOR is non-empty

proof

set i = the Element of I;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A15: C = F . the Element of I by A1;
C is Element of MSSub A by MSUALG_2:def 19;
then A16: F . the Element of I in Z by A15;
then A17: ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( F . the Element of I = Q & f . (F . the Element of I) = G & G is non-empty & G is finite-yielding ) by A9;
then reconsider G1 = f . (F . the Element of I) as finite-yielding Element of Bool the Sorts of A by A16, FUNCT_2:5;
let j be object ; :: according to PBOOLE:def 13 :: thesis: ( not j in the carrier of S or not SOR . j is empty )
assume A18: j in the carrier of S ; :: thesis: not SOR . j is empty
consider q being object such that
A19: q in G1 . j by A18, A17, XBOOLE_0:def 1;
set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
G1 c= the Sorts of A by PBOOLE:def 18;
then G1 . j c= the Sorts of A . j by A18;
then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } by A19, TARSKI:def 4;
hence not SOR . j is empty by A10, A18; :: thesis: verum

end;

then reconsider SOR = SOR as non-empty MSSubset of A ;

A20: now :: thesis: for j being set st j in the carrier of S holds
not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } is empty

set i = the Element of I;
let j be set ; :: thesis: ( j in the carrier of S implies not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } is empty )
assume A21: j in the carrier of S ; :: thesis: not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } is empty
set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A22: C = F . the Element of I by A1;
C is Element of MSSub A by MSUALG_2:def 19;
then A23: F . the Element of I in Z by A22;
then ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( F . the Element of I = Q & f . (F . the Element of I) = G & G is non-empty & G is finite-yielding ) by A9;
then reconsider G1 = f . (F . the Element of I) as finite-yielding Element of Bool the Sorts of A by A23, FUNCT_2:5;
G1 c= the Sorts of A by PBOOLE:def 18;
then G1 . j c= the Sorts of A . j by A21;
then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
hence not { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } is empty ; :: thesis: verum

end;

SOR is finite-yielding

proof

let j be object ; :: according to FINSET_1:def 5 :: thesis: ( not j in the carrier of S or SOR . j is finite )
assume A24: j in the carrier of S ; :: thesis: SOR . j is finite
set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
reconsider VV = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } as non empty set by A20, A24;

A25: now :: thesis: ex p being FinSequence st rng p = VV

defpred S₂[ set , set ] means ex L being ManySortedSet of the carrier of S st
( f . (F . $1) = L & $2 = L . j );
consider r being FinSequence such that
A26: rng r = I by FINSEQ_1:52;
A27: for a being Element of I ex b being Element of VV st S₂[a,b]

proof

let a be Element of I; :: thesis: ex b being Element of VV st S₂[a,b]
consider W being strict non-empty finitely-generated MSSubAlgebra of A such that
A28: W = F . a by A1;
W is Element of MSSub A by MSUALG_2:def 19;
then A29: W in Z by A28;
then ex Q being strict non-empty MSSubAlgebra of A ex G being GeneratorSet of Q st
( W = Q & f . W = G & G is non-empty & G is finite-yielding ) by A9;
then reconsider G1 = f . (F . a) as finite-yielding Element of Bool the Sorts of A by A28, A29, FUNCT_2:5;
G1 c= the Sorts of A by PBOOLE:def 18;
then G1 . j c= the Sorts of A . j by A24;
then G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
then reconsider b = G1 . j as Element of VV ;
take b ; :: thesis: S₂[a,b]
take G1 ; :: thesis: ( f . (F . a) = G1 & b = G1 . j )
thus ( f . (F . a) = G1 & b = G1 . j ) ; :: thesis: verum

end;

consider h being Function of I,VV such that
A30: for i being Element of I holds S₂[i,h . i] from FUNCT_2:sch 3(A27);
A31: rng r = dom h by A26, FUNCT_2:def 1;
then reconsider p = h * r as FinSequence by FINSEQ_1:16;
A32: VV c= rng p

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in VV or q in rng p )
assume q in VV ; :: thesis: q in rng p
then consider a being Element of bool ( the Sorts of A . j) such that
A33: q = a and
A34: ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) ;
consider i being Element of I, K being ManySortedSet of the carrier of S such that
A35: ( K = f . (F . i) & a = K . j ) by A34;
A36: ( rng p = rng h & dom h = I ) by A31, FUNCT_2:def 1, RELAT_1:28;
ex L being ManySortedSet of the carrier of S st
( f . (F . i) = L & h . i = L . j ) by A30;
hence q in rng p by A33, A35, A36, FUNCT_1:def 3; :: thesis: verum

end;

take p = p; :: thesis: rng p = VV
rng p c= rng h by FUNCT_1:14;
then rng p c= VV by XBOOLE_1:1;
hence rng p = VV by A32; :: thesis: verum

end;

for x being set st x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } holds
x is finite

proof

let x be set ; :: thesis: ( x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } implies x is finite )
assume x in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ; :: thesis: x is finite
then consider a being Element of bool ( the Sorts of A . j) such that
A37: x = a and
A38: ex w being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . w) & a = K . j ) ;
consider w being Element of I, K being ManySortedSet of the carrier of S such that
A39: ( K = f . (F . w) & a = K . j ) by A38;
A40: ex E being strict non-empty finitely-generated MSSubAlgebra of A st E = F . w by A1;
then F . w is Element of MSSub A by MSUALG_2:def 19;
then F . w in Z by A40;
then S₁[F . w,f . (F . w)] by A9;
hence x is finite by A37, A39; :: thesis: verum

end;

then union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } is finite by A25, FINSET_1:7;
hence SOR . j is finite by A10, A24; :: thesis: verum

end;

then reconsider SOR = SOR as non-empty finite-yielding MSSubset of A ;
take GenMSAlg SOR ; :: thesis: for i being Element of I holds F . i is MSSubAlgebra of GenMSAlg SOR
let i be Element of I; :: thesis: F . i is MSSubAlgebra of GenMSAlg SOR
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A41: C = F . i by A1;
C is Element of MSSub A by MSUALG_2:def 19;
then F . i in Z by A41;
then consider Q being strict non-empty MSSubAlgebra of A, G being GeneratorSet of Q such that
A42: F . i = Q and
A43: f . (F . i) = G and
A44: ( G is non-empty & G is finite-yielding ) by A9;
the Sorts of Q is MSSubset of A by MSUALG_2:def 9;
then ( G c= the Sorts of Q & the Sorts of Q c= the Sorts of A ) by PBOOLE:def 18;
then A45: G c= the Sorts of A by PBOOLE:13;
then reconsider G1 = G as non-empty MSSubset of A by A44, PBOOLE:def 18;
A46: G1 is ManySortedSubset of SOR

proof

let j be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not j in the carrier of S or G1 . j c= SOR . j )
assume A47: j in the carrier of S ; :: thesis: G1 . j c= SOR . j
set UU = { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } ;
G1 . j c= the Sorts of A . j by A45, A47;
then A48: G1 . j in { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } by A43;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in G1 . j or q in SOR . j )
assume q in G1 . j ; :: thesis: q in SOR . j
then q in union { a where a is Element of bool ( the Sorts of A . j) : ex i being Element of I ex K being ManySortedSet of the carrier of S st
( K = f . (F . i) & a = K . j ) } by A48, TARSKI:def 4;
hence q in SOR . j by A10, A47; :: thesis: verum

end;

C = GenMSAlg G by A41, A42, MSAFREE:3
.= GenMSAlg G1 by EXTENS_1:18 ;
hence F . i is MSSubAlgebra of GenMSAlg SOR by A41, A46, EXTENS_1:17; :: thesis: verum