let S be Language; :: thesis: for V being Element of (AllTermsOf S) * ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) *

set TT = AllTermsOf S;

set T = S -termsOfMaxDepth ;

let V be Element of (AllTermsOf S) * ; :: thesis: ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) *

deffunc H_{1}( object ) -> set = { mm where mm is Element of NAT : not V . $1 in (S -termsOfMaxDepth) . mm } ;

set B = { H_{1}(nn) where nn is Element of NAT : nn in dom V } ;

A1: dom V is finite ;

reconsider TF = S -termsOfMaxDepth as Function ;

_{1}(nn) where nn is Element of NAT : nn in dom V } is finite
from FRAENKEL:sch 21(A1);

then reconsider BB = { H_{1}(nn) where nn is Element of NAT : nn in dom V } as finite finite-membered set by A2, FINSET_1:def 6;

reconsider C = union BB as finite set ;

consider x being object such that

A5: x in NAT \ C by XBOOLE_0:def 1;

reconsider mm = x as Element of NAT by A5;

then V is FinSequence of (S -termsOfMaxDepth) . mm by FOMODEL0:26;

hence ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) * ; :: thesis: verum

set TT = AllTermsOf S;

set T = S -termsOfMaxDepth ;

let V be Element of (AllTermsOf S) * ; :: thesis: ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) *

deffunc H

set B = { H

A1: dom V is finite ;

reconsider TF = S -termsOfMaxDepth as Function ;

A2: now :: thesis: for x being set st x in { H_{1}(nn) where nn is Element of NAT : nn in dom V } holds

x is finite

{ Hx is finite

let x be set ; :: thesis: ( x in { H_{1}(nn) where nn is Element of NAT : nn in dom V } implies x is finite )

assume x in { H_{1}(nn) where nn is Element of NAT : nn in dom V }
; :: thesis: x is finite

then consider nn being Element of NAT such that

A3: ( x = { mm where mm is Element of NAT : not V . nn in (S -termsOfMaxDepth) . mm } & nn in dom V ) ;

reconsider D = dom V as non empty set by A3;

rng V c= AllTermsOf S by RELAT_1:def 19;

then reconsider VV = V as Function of D,(AllTermsOf S) by FUNCT_2:2;

reconsider nnn = nn as Element of D by A3;

consider kk being Element of NAT such that

A4: VV . nnn in TF . kk by FOMODEL1:5;

x c= kk by Lm2, A3, A4;

hence x is finite ; :: thesis: verum

end;assume x in { H

then consider nn being Element of NAT such that

A3: ( x = { mm where mm is Element of NAT : not V . nn in (S -termsOfMaxDepth) . mm } & nn in dom V ) ;

reconsider D = dom V as non empty set by A3;

rng V c= AllTermsOf S by RELAT_1:def 19;

then reconsider VV = V as Function of D,(AllTermsOf S) by FUNCT_2:2;

reconsider nnn = nn as Element of D by A3;

consider kk being Element of NAT such that

A4: VV . nnn in TF . kk by FOMODEL1:5;

x c= kk by Lm2, A3, A4;

hence x is finite ; :: thesis: verum

then reconsider BB = { H

reconsider C = union BB as finite set ;

consider x being object such that

A5: x in NAT \ C by XBOOLE_0:def 1;

reconsider mm = x as Element of NAT by A5;

now :: thesis: for i being object st i in dom V holds

V . i in (S -termsOfMaxDepth) . mm

then
V is Function of (dom V),((S -termsOfMaxDepth) . mm)
by FUNCT_2:3;V . i in (S -termsOfMaxDepth) . mm

let i be object ; :: thesis: ( i in dom V implies V . i in (S -termsOfMaxDepth) . mm )

assume A6: i in dom V ; :: thesis: V . i in (S -termsOfMaxDepth) . mm

then reconsider ii = i as Element of NAT ;

( not V . i in (S -termsOfMaxDepth) . mm implies mm in C )

end;assume A6: i in dom V ; :: thesis: V . i in (S -termsOfMaxDepth) . mm

then reconsider ii = i as Element of NAT ;

( not V . i in (S -termsOfMaxDepth) . mm implies mm in C )

proof

hence
V . i in (S -termsOfMaxDepth) . mm
by A5, XBOOLE_0:def 5; :: thesis: verum
assume
not V . i in (S -termsOfMaxDepth) . mm
; :: thesis: mm in C

then ( mm in H_{1}(i) & H_{1}(ii) in { H_{1}(nn) where nn is Element of NAT : nn in dom V } )
by A6;

hence mm in C by TARSKI:def 4; :: thesis: verum

end;then ( mm in H

hence mm in C by TARSKI:def 4; :: thesis: verum

then V is FinSequence of (S -termsOfMaxDepth) . mm by FOMODEL0:26;

hence ex mm being Element of NAT st V is Element of ((S -termsOfMaxDepth) . mm) * ; :: thesis: verum