let S be non empty non void ManySortedSign ; :: thesis: for I being non empty finite set
for A being non-empty MSAlgebra of 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 of 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 of 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 J = the carrier of S;
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 ) } ;
consider m being Element of I;
consider W being strict non-empty finitely-generated MSSubAlgebra of A such that
A2: W = F . m by A1;
W is Element of MSSub A by MSUALG_2:def 20;
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
A6: ( C = F . i & C = D ) by A5;
consider G being GeneratorSet of D such that
A7: G is finite-yielding by MSAFREE2:def 10;
consider S being V2() V26() ManySortedSubset of the Sorts of D such that
A8: G c= S by A7, MSUALG_9:8;
S is ManySortedSubset of the Sorts of A

proof

A9: S c= the Sorts of D by PBOOLE:def 23;
the Sorts of D is MSSubset of A by MSUALG_2:def 10;
then the Sorts of D c= the Sorts of A by PBOOLE:def 23;
hence S c= the Sorts of A by A9, PBOOLE:15; :: according to PBOOLE:def 23 :: thesis: verum

end;

then reconsider b = S as Element of Bool the Sorts of A by CLOSURE2:def 1;
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 )
reconsider S = S as GeneratorSet of D by A8, MSSCYC_1:21;
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
A10: for B being Element of Z holds S₁[B,f . B] from FUNCT_2:sch 3(A3);
deffunc H₁( set ) -> 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 st
( K = f . (F . i) & a = K . $1 ) } ;
consider SOR being ManySortedSet of such that
A11: for j being set 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 set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not j in the carrier of S or SOR . j c= the Sorts of A . j )
assume A12: j in the carrier of S ; :: thesis: SOR . j c= 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 st
( K = f . (F . i) & a = K . j ) } ;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in SOR . j or q in the Sorts of A . 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 st
( K = f . (F . i) & a = K . j ) } by A11, A12;
then consider w being set such that
A13: q in w and
A14: 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 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
A15: w = a and
ex i being Element of I ex K being ManySortedSet of st
( K = f . (F . i) & a = K . j ) by A14;
thus q in the Sorts of A . j by A13, A15; :: thesis: verum

end;

then reconsider SOR = SOR as MSSubset of A ;

A16: now

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 st
( K = f . (F . i) & a = K . j ) } is empty )
assume A17: 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 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 st
( K = f . (F . i) & a = K . j ) } ;
consider i being Element of I;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A18: C = F . i by A1;
C is Element of MSSub A by MSUALG_2:def 20;
then A19: F . i in Z by A18;
then consider Q being strict non-empty MSSubAlgebra of A such that
A20: ex G being GeneratorSet of Q st
( F . i = Q & f . (F . i) = G & G is non-empty & G is finite-yielding ) by A10;
reconsider G1 = f . (F . i) as V26() Element of Bool the Sorts of A by A19, A20, FUNCT_2:7;
G1 c= the Sorts of A by PBOOLE:def 23;
then G1 . j c= the Sorts of A . j by A17, PBOOLE:def 5;
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 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 st
( K = f . (F . i) & a = K . j ) } is empty ; :: thesis: verum

end;

SOR is non-empty

proof

let j be set ; :: according to PBOOLE:def 16 :: thesis: ( not j in the carrier of S or not SOR . j is empty )
assume A21: j in the carrier of S ; :: thesis: not SOR . 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 st
( K = f . (F . i) & a = K . j ) } ;
consider i being Element of I;
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A22: C = F . i by A1;
C is Element of MSSub A by MSUALG_2:def 20;
then A23: F . i in Z by A22;
then consider Q being strict non-empty MSSubAlgebra of A such that
A24: ex G being GeneratorSet of Q st
( F . i = Q & f . (F . i) = G & G is non-empty & G is finite-yielding ) by A10;
reconsider G1 = f . (F . i) as V26() Element of Bool the Sorts of A by A23, A24, FUNCT_2:7;
G1 c= the Sorts of A by PBOOLE:def 23;
then G1 . j c= the Sorts of A . j by A21, PBOOLE:def 5;
then A25: 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 st
( K = f . (F . i) & a = K . j ) } ;
not G1 . j is empty by A21, A24;
then consider q being set such that
A26: q in G1 . j by XBOOLE_0:def 1;
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 st
( K = f . (F . i) & a = K . j ) } by A25, A26, TARSKI:def 4;
hence not SOR . j is empty by A11, A21; :: thesis: verum

end;

then reconsider SOR = SOR as V2() MSSubset of A ;
SOR is finite-yielding

proof

let j be set ; :: according to FINSET_1:def 4 :: thesis: ( not j in the carrier of S or SOR . j is finite )
assume A27: 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 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 st
( K = f . (F . i) & a = K . j ) } as non empty set by A16, A27;

A28: now

consider r being FinSequence such that
A29: rng r = I by FINSEQ_1:73;
defpred S₂[ set , set ] means ex L being ManySortedSet of st
( f . (F . $1) = L & $2 = L . j );
A30: 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
A31: W = F . a by A1;
W is Element of MSSub A by MSUALG_2:def 20;
then A32: W in Z by A31;
then consider Q being strict non-empty MSSubAlgebra of A such that
A33: ex G being GeneratorSet of Q st
( W = Q & f . W = G & G is non-empty & G is finite-yielding ) by A10;
reconsider G1 = f . (F . a) as V26() Element of Bool the Sorts of A by A31, A32, A33, FUNCT_2:7;
G1 c= the Sorts of A by PBOOLE:def 23;
then G1 . j c= the Sorts of A . j by A27, PBOOLE:def 5;
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 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
A34: for i being Element of I holds S₂[i,h . i] from FUNCT_2:sch 3(A30);
A35: rng r = dom h by A29, FUNCT_2:def 1;
then reconsider p = h * r as FinSequence by FINSEQ_1:20;
take p = p; :: thesis: rng p = VV
thus rng p = VV :: thesis: verum

proof

rng p c= rng h

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in rng p or q in rng h )
assume q in rng p ; :: thesis: q in rng h
hence q in rng h by FUNCT_1:25; :: thesis: verum

end;

hence rng p c= VV by XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: VV c= rng p
thus VV c= rng p :: thesis: verum

proof

let q be set ; :: 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
A36: q = a and
A37: ex i being Element of I ex K being ManySortedSet of st
( K = f . (F . i) & a = K . j ) ;
consider i being Element of I, K being ManySortedSet of such that
A38: ( K = f . (F . i) & a = K . j ) by A37;
A39: rng p = rng h by A35, RELAT_1:47;
A40: dom h = I by FUNCT_2:def 1;
ex L being ManySortedSet of st
( f . (F . i) = L & h . i = L . j ) by A34;
hence q in rng p by A36, A38, A39, A40, FUNCT_1:def 5; :: thesis: verum

end;

end;

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 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 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 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
A41: x = a and
A42: ex w being Element of I ex K being ManySortedSet of st
( K = f . (F . w) & a = K . j ) ;
consider w being Element of I, K being ManySortedSet of such that
A43: ( K = f . (F . w) & a = K . j ) by A42;
consider E being strict non-empty finitely-generated MSSubAlgebra of A such that
A44: E = F . w by A1;
F . w is Element of MSSub A by A44, MSUALG_2:def 20;
then F . w in Z by A44;
then S₁[F . w,f . (F . w)] by A10;
then consider Q being strict non-empty MSSubAlgebra of A such that
F . w = Q and
A45: ex G being GeneratorSet of Q st
( f . (F . w) = G & G is finite-yielding ) ;
thus x is finite by A27, A41, A43, A45, FINSET_1:def 4; :: 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 st
( K = f . (F . i) & a = K . j ) } is finite by A28, FINSET_1:25;
hence SOR . j is finite by A11, A27; :: thesis: verum

end;

then reconsider SOR = SOR as V2() V26() MSSubset of A ;
take B = GenMSAlg SOR; :: thesis: for i being Element of I holds F . i is MSSubAlgebra of B
let i be Element of I; :: thesis: F . i is MSSubAlgebra of B
consider C being strict non-empty finitely-generated MSSubAlgebra of A such that
A46: C = F . i by A1;
C is Element of MSSub A by MSUALG_2:def 20;
then F . i in Z by A46;
then consider Q being strict non-empty MSSubAlgebra of A, G being GeneratorSet of Q such that
A47: F . i = Q and
A48: ( f . (F . i) = G & G is non-empty & G is finite-yielding ) by A10;
A49: G c= the Sorts of Q by PBOOLE:def 23;
the Sorts of Q is MSSubset of A by MSUALG_2:def 10;
then the Sorts of Q c= the Sorts of A by PBOOLE:def 23;
then A50: G c= the Sorts of A by A49, PBOOLE:15;
then reconsider G1 = G as V2() MSSubset of A by A48, PBOOLE:def 23;
A51: G1 is ManySortedSubset of SOR

proof

let j be set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not j in the carrier of S or G1 . j c= SOR . j )
assume A52: 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 st
( K = f . (F . i) & a = K . j ) } ;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in G1 . j or q in SOR . j )
assume A53: q in G1 . j ; :: thesis: q in SOR . j
G1 . j c= the Sorts of A . j by A50, A52, PBOOLE:def 5;
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 st
( K = f . (F . i) & a = K . j ) } by A48;
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 st
( K = f . (F . i) & a = K . j ) } by A53, TARSKI:def 4;
hence q in SOR . j by A11, A52; :: thesis: verum

end;

C = GenMSAlg G by A46, A47, MSAFREE:3
.= GenMSAlg G1 by EXTENS_1:22 ;
hence F . i is MSSubAlgebra of B by A46, A51, EXTENS_1:21; :: thesis: verum