let S be non empty non void ManySortedSign ; :: thesis: for X being V2() V39() ManySortedSet of the carrier of S st S is finitely_operated holds

for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite

let X be V2() V39() ManySortedSet of the carrier of S; :: thesis: ( S is finitely_operated implies for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite )

assume A1: S is finitely_operated ; :: thesis: for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite

set SF = the Sorts of (FreeMSA X);

defpred S_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A54, A3); :: thesis: verum

for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite

let X be V2() V39() ManySortedSet of the carrier of S; :: thesis: ( S is finitely_operated implies for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite )

assume A1: S is finitely_operated ; :: thesis: for n being Nat

for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite

set SF = the Sorts of (FreeMSA X);

defpred S

A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;

A3: for k being Nat st S

S

proof

A54:
S
deffunc H_{1}( set ) -> set = $1;

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

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: S_{1}[n + 1]

let v be SortSymbol of S; :: thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite

defpred S_{2}[ Element of the Sorts of (FreeMSA X) . v] means depth $1 = n + 1;

defpred S_{3}[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n + 1;

defpred S_{4}[ Element of the Sorts of (FreeMSA X) . v] means ( depth $1 <= n or depth $1 = n + 1 );

set dn1 = { H_{1}(t) where t is Element of the Sorts of (FreeMSA X) . v : S_{3}[t] } ;

set dn11 = { H_{1}(t) where t is Element of the Sorts of (FreeMSA X) . v : S_{4}[t] } ;

set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S_{2}[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_{2}( 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_{2}(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_{2}[t] } c= Union dvs

dvs . k is finite

defpred S_{5}[ 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_{5}[t] } ;

A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S_{5}[t] or S_{2}[t] ) } = { t where t is Element of the Sorts of (FreeMSA X) . v : S_{5}[t] } \/ { t where t is Element of the Sorts of (FreeMSA X) . v : S_{2}[t] }
from TOPREAL1:sch 1();

A52: for t being Element of the Sorts of (FreeMSA X) . v holds

( S_{3}[t] iff S_{4}[t] )
by NAT_1:8, NAT_1:12;

A53: { H_{1}(t) where t is Element of the Sorts of (FreeMSA X) . v : S_{3}[t] } = { H_{1}(t) where t is Element of the Sorts of (FreeMSA X) . v : S_{4}[t] }
from FRAENKEL:sch 3(A52);

{ t where t is Element of the Sorts of (FreeMSA X) . v : S_{5}[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: verum

end;let n be Nat; :: thesis: ( S

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: S

let v be SortSymbol of S; :: thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite

defpred S

defpred S

defpred S

set dn1 = { H

set dn11 = { H

set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S

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

consider dvs being FinSequence such that

A7: ( len dvs = len ovs & ( for k being Nat st k in dom dvs holds

dvs . k = H

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

proof

for k being object st k in dom dvs holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : S_{2}[t] } or x in Union dvs )

assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S_{2}[t] }
; :: thesis: x in Union dvs

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;

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: verum

end;assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S

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: not t9 is root

then consider o being OperSymbol of S such that 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: contradiction

hence contradiction by A12, A13, TREES_1:42, TREES_9:def 1; :: thesis: verum

end;( dt = t & tt = dom dt & depth t = height tt ) by MSAFREE2:def 14;

assume t9 is root ; :: thesis: contradiction

hence contradiction by A12, A13, TREES_1:42, TREES_9:def 1; :: thesis: verum

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: verum

dvs . k is finite

proof

then A50:
Union dvs is finite
by CARD_2:88;
let k be object ; :: thesis: ( k in dom dvs implies dvs . k is finite )

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: dvs . k is finite

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 ) ) }_{3}( 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

A38: ( len nS = len (the_arity_of o) & ( for k being Nat st k in dom nS holds

nS . k = H_{3}(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

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: verum

end;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: dvs . k is finite

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

deffunc H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not 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] ) } or 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 ) ) } )

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: 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 ) ) }

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: verum

end;( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } )

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: 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 ) ) }

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: verum

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

consider nS being FinSequence such that
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: ( ( for b_{1} being object holds

( not b_{1} 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 ) ) } or ex b_{2} being object st

( b_{2} 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 ) ) } & [b_{1},b_{2}] 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 ) ) } ) ) ) & ( for b_{1} being object holds

( not b_{1} 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 ) ) } or ex b_{2} being object st

( b_{2} 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 ) ) } & [b_{2},b_{1}] 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 ) ) } ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] 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 ) ) } or not [b_{3},b_{4}] 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 ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [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 ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )

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: ( not [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 ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )

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: ( ( not x = z or y = u ) & ( not y = u or x = z ) )

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: ( not y = u or x = z )

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: x = z

hence x = z by A31, A34, A32, A37, A35, A36, TREES_4:15; :: thesis: verum

end;( 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: ( ( for b

( not b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b

( b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b

( not b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b

( b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b

( not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b

hereby :: thesis: ( ( for b_{1} being object holds

( not b_{1} 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 ) ) } or ex b_{2} being object st

( b_{2} 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 ) ) } & [b_{2},b_{1}] 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 ) ) } ) ) ) & ( for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] 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 ) ) } or not [b_{3},b_{4}] 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 ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) ) ) )

( not b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b

( b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b

( not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b

let x be object ; :: thesis: ( 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 ) ) } implies ex y9 being object st

( 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 ) ) } & [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 ) ) } ) )

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: ex y9 being object st

( 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 ) ) } & [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 ) ) } )

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: ( 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 ) ) } & [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 ) ) } )

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: [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 ) ) }

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: verum

end;( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex y9 being object st

( 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 ) ) } & [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 ) ) } ) )

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: ex y9 being object st

( 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 ) ) } & [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 ) ) } )

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: ( 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 ) ) } & [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 ) ) } )

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: [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 ) ) }

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: verum

hereby :: thesis: for b_{1}, b_{2}, b_{3}, b_{4} being object holds

( not [b_{1},b_{2}] 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 ) ) } or not [b_{3},b_{4}] 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 ) ) } or ( ( not b_{1} = b_{3} or b_{2} = b_{4} ) & ( not b_{2} = b_{4} or b_{1} = b_{3} ) ) )

let x, y, z, u be object ; :: thesis: ( not [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 ( not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b

let y be object ; :: thesis: ( 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 ) ) } implies ex a9 being object st

( 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 ) ) } & [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 ) ) } ) )

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: ex a9 being object st

( 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 ) ) } & [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 ) ) } )

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: ( 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 ) ) } & [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 ) ) } )

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: [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 ) ) }

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: verum

end;( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex a9 being object st

( 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 ) ) } & [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 ) ) } ) )

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: ex a9 being object st

( 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 ) ) } & [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 ) ) } )

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: ( 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 ) ) } & [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 ) ) } )

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: [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 ) ) }

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: verum

( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [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 ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )

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: ( not [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 ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )

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: ( ( not x = z or y = u ) & ( not y = u or x = z ) )

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: ( not y = u or x = z )

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: x = z

hence x = z by A31, A34, A32, A37, A35, A36, TREES_4:15; :: thesis: verum

A38: ( len nS = len (the_arity_of o) & ( for k being Nat st k in dom nS holds

nS . k = H

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: ( not 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 ) ) } or x in product nS )

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: x in product nS

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;

end;( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or x in product nS )

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: x in product nS

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: for x being object st x in dom a holds

a . x in nS . x

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

let x be object ; :: thesis: ( x in dom a implies a . x in nS . x )

assume A46: x in dom a ; :: thesis: a . x in nS . x

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: verum

end;assume A46: x in dom a ; :: thesis: a . x in nS . x

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: verum

now :: thesis: for x being object st x in dom nS holds

nS . x is finite

then
nS is V39()
by FINSET_1:def 4;nS . x is finite

let x be object ; :: thesis: ( x in dom nS implies nS . x is finite )

assume A49: x in dom nS ; :: thesis: nS . x is finite

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: verum

end;assume A49: x in dom nS ; :: thesis: nS . x is finite

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: verum

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: verum

defpred S

set dln = { t where t is Element of the Sorts of (FreeMSA X) . v : S

A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S

A52: for t being Element of the Sorts of (FreeMSA X) . v holds

( S

A53: { H

{ t where t is Element of the Sorts of (FreeMSA X) . v : S

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: verum

proof

thus
for n being Nat holds S
let v be SortSymbol of S; :: thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite

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 }

hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite by A55; :: thesis: verum

end;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

( 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;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } )

assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; :: thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }

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: verum

end;assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; :: thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 }

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: verum

hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite by A55; :: thesis: verum