let S be non empty non void ManySortedSign ; :: thesis:
let X be non-empty finite-yielding ManySortedSet of the carrier of S; :: thesis:
assume A1: S is finitely_operated ; :: thesis:
set SF = the Sorts of (FreeMSA X);
defpred S₁[ Nat] means for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= $1 } is finite ;
A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

deffunc H₁( set ) -> set = $1;
let n be Nat; :: thesis:
assume A4: for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite ; :: thesis:
let v be SortSymbol of S; :: thesis:
defpred S₂[ Element of the Sorts of (FreeMSA X) . v] means depth $1 = n + 1;
defpred S₃[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n + 1;
defpred S₄[ Element of the Sorts of (FreeMSA X) . v] means ( depth $1 <= n or depth $1 = n + 1 );
set dn1 = { H₁(t) where t is Element of the Sorts of (FreeMSA X) . v : S₃[t] } ;
set dn11 = { H₁(t) where t is Element of the Sorts of (FreeMSA X) . v : S₄[t] } ;
set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S₂[t] } ;
set ov = { o where o is OperSymbol of S : the_result_sort_of o = v } ;
A5: the Sorts of (FreeMSA X) . v = FreeSort (X,v) by A2, MSAFREE:def 11;
{ o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, MSSCYC_1:def 5;
then consider ovs being FinSequence such that
A6: rng ovs = { o where o is OperSymbol of S : the_result_sort_of o = v } by FINSEQ_1:52;
deffunc H₂( set ) -> set = { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . $1), the carrier of S] ) } ;
consider dvs being FinSequence such that
A7: ( len dvs = len ovs & ( for k being Nat st k in dom dvs holds
dvs . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A8: ( dom ovs = Seg (len ovs) & dom dvs = Seg (len dvs) ) by FINSEQ_1:def 3;
A9: FreeSort (X,v) c= S -Terms X by MSATERM:12;
A10: { t where t is Element of the Sorts of (FreeMSA X) . v : S₂[t] } c= Union dvs

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S₂[t] } ; :: thesis:
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A11: x = t and
A12: depth t = n + 1 ;
t in FreeSort (X,v) by A5;
then reconsider t9 = t as Term of S,X by A9;

now :: thesis:

A13: ex dt being finite DecoratedTree ex tt being finite Tree st
( dt = t & tt = dom dt & depth t = height tt ) by MSAFREE2:def 14;
assume t9 is root ; :: thesis:
hence contradiction by A12, A13, TREES_1:42, TREES_9:def 1; :: thesis:

end;

then consider o being OperSymbol of S such that
A14: t9 . {} = [o, the carrier of S] by MSSCYC_1:20;
the_result_sort_of o = the_sort_of t9 by A14, MSATERM:17
.= v by A5, MSATERM:def 5 ;
then o in rng ovs by A6;
then consider k being object such that
A15: k in dom ovs and
A16: o = ovs . k by FUNCT_1:def 3;
dvs . k = { t1 where t1 is Element of the Sorts of (FreeMSA X) . v : ( depth t1 = n + 1 & t1 . {} = [(ovs . k), the carrier of S] ) } by A7, A8, A15;
then A17: t in dvs . k by A12, A14, A16;
dvs . k in rng dvs by A7, A8, A15, FUNCT_1:def 3;
then t in union (rng dvs) by A17, TARSKI:def 4;
hence x in Union dvs by A11, CARD_3:def 4; :: thesis:

end;

for k being object st k in dom dvs holds
dvs . k is finite

proof

let k be object ; :: thesis:
set dvsk = { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ;
assume A18: k in dom dvs ; :: thesis:
then ovs . k in rng ovs by A7, A8, FUNCT_1:def 3;
then consider o being OperSymbol of S such that
A19: o = ovs . k and
the_result_sort_of o = v by A6;
set davsk = { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
A20: { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } c= { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ; :: thesis:
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A21: x = t and
A22: depth t = n + 1 and
A23: t . {} = [o, the carrier of S] by A19;
t in FreeSort (X,v) by A5;
then reconsider t9 = t as Term of S,X by A9;
consider a being ArgumentSeq of Sym (o,X) such that
A24: t9 = [o, the carrier of S] -tree a by A23, MSATERM:10;
reconsider a9 = a as Element of (S -Terms X) * by FINSEQ_1:def 11;
[o, the carrier of S] -tree a9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A22, A24;
hence x in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A21, A24; :: thesis:

end;

deffunc H₃( Nat) -> set = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. $1) : depth t <= n } ;
set avsk = { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
A25: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } , { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } are_equipotent

proof

set Z = { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ;
take { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: according to TARSKI:def 6 :: thesis:

hereby :: thesis:

let x be object ; :: thesis:
assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: thesis:
then consider a being Element of (S -Terms X) * such that
A26: x = a and
A27: ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ;
reconsider y9 = [o, the carrier of S] -tree a as object ;
take y9 = y9; :: thesis:
thus y9 in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A27; :: thesis:
thus [x,y9] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A26, A27; :: thesis:

end;

hereby :: thesis:

let y be object ; :: thesis:
assume y in { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: thesis:
then consider a being Element of (S -Terms X) * such that
A28: y = [o, the carrier of S] -tree a and
A29: ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ;
reconsider a9 = a as object ;
take a9 = a9; :: thesis:
thus a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A29; :: thesis:
thus [a9,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A28, A29; :: thesis:

end;

let x, y, z, u be object ; :: thesis:
assume [x,y] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: thesis:
then consider xa being Element of (S -Terms X) * such that
A30: [x,y] = [xa,([o, the carrier of S] -tree xa)] and
A31: xa is ArgumentSeq of Sym (o,X) and
ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree xa ) ;
A32: x = xa by A30, XTUPLE_0:1;
assume [z,u] in { [a,([o, the carrier of S] -tree a)] where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: thesis:
then consider za being Element of (S -Terms X) * such that
A33: [z,u] = [za,([o, the carrier of S] -tree za)] and
A34: za is ArgumentSeq of Sym (o,X) and
ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree za ) ;
A35: z = za by A33, XTUPLE_0:1;
hence ( x = z implies y = u ) by A30, A33, A32, XTUPLE_0:1; :: thesis:
A36: u = [o, the carrier of S] -tree za by A33, XTUPLE_0:1;
A37: y = [o, the carrier of S] -tree xa by A30, XTUPLE_0:1;
assume y = u ; :: thesis:
hence x = z by A31, A34, A32, A37, A35, A36, TREES_4:15; :: thesis:

end;

consider nS being FinSequence such that
A38: ( len nS = len (the_arity_of o) & ( for k being Nat st k in dom nS holds
nS . k = H₃(k) ) ) from FINSEQ_1:sch 2();
A39: dom nS = Seg (len nS) by FINSEQ_1:def 3;
A40: dom nS = Seg (len (the_arity_of o)) by A38, FINSEQ_1:def 3;
A41: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } c= product nS

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: thesis:
then consider a being Element of (S -Terms X) * such that
A42: x = a and
A43: a is ArgumentSeq of Sym (o,X) and
A44: ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ;
reconsider a = a as ArgumentSeq of Sym (o,X) by A43;
A45: ( len a = len (the_arity_of o) & dom a = Seg (len a) ) by FINSEQ_1:def 3, MSATERM:22;

now :: thesis:

let x be object ; :: thesis:
assume A46: x in dom a ; :: thesis:
then reconsider k = x as Element of NAT ;
reconsider ak = a . k as Term of S,X by A46, MSATERM:22;
A47: the_sort_of ak = (the_arity_of o) /. k by A46, MSATERM:23;
the Sorts of (FreeMSA X) . (the_sort_of ak) = FreeSort (X,(the_sort_of ak)) by A2, MSAFREE:def 11;
then reconsider ak = ak as Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) by A47, MSATERM:def 5;
depth ak < n + 1 by A44, A46, MSSCYC_1:27;
then A48: depth ak <= n by NAT_1:13;
set nSk = { tk where tk is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } ;
{ tk where tk is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } = nS . x by A38, A40, A45, A46;
hence a . x in nS . x by A48; :: thesis:

end;

hence x in product nS by A38, A39, A42, A45, CARD_3:def 5; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
assume A49: x in dom nS ; :: thesis:
then reconsider k = x as Nat ;
set nSk = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } ;
nS . k = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } by A38, A49;
hence nS . x is finite by A4; :: thesis:

end;

then nS is finite-yielding by FINSET_1:def 4;
then product nS is finite ;
then { ([o, the carrier of S] -tree a) where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st
( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } is finite by A25, A41, CARD_1:38;
hence dvs . k is finite by A7, A18, A20; :: thesis:

end;

then A50: Union dvs is finite by CARD_2:88;
defpred S₅[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n;
set dln = { t where t is Element of the Sorts of (FreeMSA X) . v : S₅[t] } ;
A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S₅[t] or S₂[t] ) } = { t where t is Element of the Sorts of (FreeMSA X) . v : S₅[t] } \/ { t where t is Element of the Sorts of (FreeMSA X) . v : S₂[t] } from TOPREAL1:sch 1();
A52: for t being Element of the Sorts of (FreeMSA X) . v holds
( S₃[t] iff S₄[t] ) by NAT_1:8, NAT_1:12;
A53: { H₁(t) where t is Element of the Sorts of (FreeMSA X) . v : S₃[t] } = { H₁(t) where t is Element of the Sorts of (FreeMSA X) . v : S₄[t] } from FRAENKEL:sch 3(A52);
{ t where t is Element of the Sorts of (FreeMSA X) . v : S₅[t] } is finite by A4;
hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite by A53, A51, A50, A10; :: thesis:

end;

A54: S₁[ 0 ]

proof

let v be SortSymbol of S; :: thesis:
set dle0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ;
set d0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ;
A55: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; :: thesis:
then consider t being Element of the Sorts of (FreeMSA X) . v such that
A56: x = t and
A57: depth t <= 0 ;
depth t = 0 by A57;
hence x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A56; :: thesis:

end;

( Constants ((FreeMSA X),v) is finite & { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) ) by A1, MSSCYC_1:25, MSSCYC_1:26;
hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite by A55; :: thesis:

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A54, A3); :: thesis: