let S be non empty non void ManySortedSign ; 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 ; 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; 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; ( ( 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
; 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 S1[ 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 V2() & G is V32() );
A3:
for a being Element of Z ex b being Element of Bool the Sorts of A st S1[a,b]
consider f being Function of Z,(Bool the Sorts of A) such that
A9:
for B being Element of Z holds S1[B,f . B]
from FUNCT_2:sch 3(A3);
deffunc H1( 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 = H1(j)
from PBOOLE:sch 4();
SOR is ManySortedSubset of the Sorts of A
then reconsider SOR = SOR as MSSubset of A ;
SOR is V2()
then reconsider SOR = SOR as V2() MSSubset of A ;
SOR is V32()
then reconsider SOR = SOR as V2() V32() MSSubset of A ;
take
GenMSAlg SOR
; for i being Element of I holds F . i is MSSubAlgebra of GenMSAlg SOR
let i be Element of I; 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 V2() & G is V32() )
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 V2() MSSubset of A by A44, PBOOLE:def 18;
A46:
G1 is ManySortedSubset of SOR
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; verum