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₁( object ) -> set = { mm where mm is Element of NAT : not V . $1 in (S -termsOfMaxDepth) . mm } ;
set B = { H₁(nn) where nn is Element of NAT : nn in dom V } ;
A1: dom V is finite ;
reconsider TF = S -termsOfMaxDepth as Function ;

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

let x be set ; :: thesis: ( x in { H₁(nn) where nn is Element of NAT : nn in dom V } implies x is finite )
assume x in { H₁(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;

{ H₁(nn) where nn is Element of NAT : nn in dom V } is finite from FRAENKEL:sch 21(A1);
then reconsider BB = { H₁(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;

now :: thesis: for i being object st i in dom V holds
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 )

proof

assume not V . i in (S -termsOfMaxDepth) . mm ; :: thesis: mm in C
then ( mm in H₁(i) & H₁(ii) in { H₁(nn) where nn is Element of NAT : nn in dom V } ) by A6;
hence mm in C by TARSKI:def 4; :: thesis: verum

end;

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

end;

then V is Function of (dom V),((S -termsOfMaxDepth) . mm) by FUNCT_2:3;
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