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 S1[ 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 S1[k] holds
S1[k + 1]
proof
deffunc H1( set ) -> set = $1;
let n be Nat; :: thesis: ( S1[n] implies S1[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: S1[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 S2[ Element of the Sorts of (FreeMSA X) . v] means depth $1 = n + 1;
defpred S3[ Element of the Sorts of (FreeMSA X) . v] means depth $1 <= n + 1;
defpred S4[ Element of the Sorts of (FreeMSA X) . v] means ( depth $1 <= n or depth $1 = n + 1 );
set dn1 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } ;
set dn11 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } ;
set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S2[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 H2( 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 = H2(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 : S2[t] } c= Union dvs
proof
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 : S2[t] } or x in Union dvs )
assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S2[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;
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: verum
end;
for k being object st k in dom dvs holds
dvs . k is finite
proof
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 ) ) }
proof
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;
deffunc H3( 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: ( ( for b1 being object holds
( not b1 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 b2 being object st
( b2 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 ) ) } & [b1,b2] 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 b1 being object holds
( not b1 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 b2 being object st
( b2 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 ) ) } & [b2,b1] 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 b1, b2, b3, b4 being object holds
( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
hereby :: thesis: ( ( for b1 being object holds
( not b1 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 b2 being object st
( b2 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 ) ) } & [b2,b1] 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 b1, b2, b3, b4 being object holds
( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
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;
hereby :: thesis: for b1, b2, b3, b4 being object holds
( not [b1,b2] 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 [b3,b4] 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 b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
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;
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
( 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;
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 = H3(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: ( 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;
now :: thesis: for x being object st x in dom a holds
a . 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;
hence x in product nS by A38, A39, A42, A45, CARD_3:def 5; :: thesis: verum
end;
now :: thesis: for x being object st x in dom nS holds
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;
then nS is V39() 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: verum
end;
then A50: Union dvs is finite by CARD_2:88;
defpred S5[ 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 : S5[t] } ;
A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S5[t] or S2[t] ) } = { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } \/ { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } from TOPREAL1:sch 1();
 A52: for t being Element of the Sorts of (FreeMSA X) . v holds
( S3[t] iff S4[t] ) by NAT_1:8, NAT_1:12;
A53: { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } from FRAENKEL:sch 3(A52);
 { t where t is Element of the Sorts of (FreeMSA X) . v : S5[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;
A54: S1[ 0 ]
proof
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 }
proof
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;
( 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: verum
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A54, A3); :: thesis: verum