set C = S -multiCat ;

set t = s -compound V;

set T = S -termsOfMaxDepth ;

set L = LettersOf S;

set SS = AllSymbolsOf S;

set n = |.(ar s).|;

set A = AtomicTermsOf S;

set fam = { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ;

A1: V is FinSequence of (S -termsOfMaxDepth) . mm by FINSEQ_1:def 11;

reconsider Ss = ((AllSymbolsOf S) *) \ {{}} as Subset of ((AllSymbolsOf S) *) ;

V in Ss * ;

then reconsider VV = V as Element of ((AllSymbolsOf S) *) * ;

( s -compound V = <*s*> ^ ((S -multiCat) . VV) & rng VV c= (S -termsOfMaxDepth) . mm ) by A1, FINSEQ_1:def 4;

then A2: s -compound V in Compound (s,((S -termsOfMaxDepth) . mm)) ;

set t = s -compound V;

set T = S -termsOfMaxDepth ;

set L = LettersOf S;

set SS = AllSymbolsOf S;

set n = |.(ar s).|;

set A = AtomicTermsOf S;

set fam = { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ;

A1: V is FinSequence of (S -termsOfMaxDepth) . mm by FINSEQ_1:def 11;

reconsider Ss = ((AllSymbolsOf S) *) \ {{}} as Subset of ((AllSymbolsOf S) *) ;

V in Ss * ;

then reconsider VV = V as Element of ((AllSymbolsOf S) *) * ;

( s -compound V = <*s*> ^ ((S -multiCat) . VV) & rng VV c= (S -termsOfMaxDepth) . mm ) by A1, FINSEQ_1:def 4;

then A2: s -compound V in Compound (s,((S -termsOfMaxDepth) . mm)) ;

per cases
( s is literal or not s is literal )
;

end;

suppose
s is literal
; :: thesis: for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is mm + 1 -termal

b

then reconsider v = s as literal Element of S ;

reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;

ar v = 0 ;

then |.(ar s).| = 0 ;

then reconsider VVV = V as 0 -element FinSequence ;

s -compound V = <*s*> ^ VVV

.= <*vv*> ;

then s -compound V in AtomicTermsOf S by FINSEQ_2:98;

then ( (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + (mm + 1)) & s -compound V in (S -termsOfMaxDepth) . 0 ) by FOMODEL1:def 30, FOMODEL1:4;

hence for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is mm + 1 -termal
; :: thesis: verum

end;reconsider vv = v as Element of LettersOf S by FOMODEL1:def 14;

ar v = 0 ;

then |.(ar s).| = 0 ;

then reconsider VVV = V as 0 -element FinSequence ;

s -compound V = <*s*> ^ VVV

.= <*vv*> ;

then s -compound V in AtomicTermsOf S by FINSEQ_2:98;

then ( (S -termsOfMaxDepth) . 0 c= (S -termsOfMaxDepth) . (0 + (mm + 1)) & s -compound V in (S -termsOfMaxDepth) . 0 ) by FOMODEL1:def 30, FOMODEL1:4;

hence for b

b

suppose
not s is literal
; :: thesis: for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is mm + 1 -termal

b

then
Compound (s,((S -termsOfMaxDepth) . mm)) in { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational }
;

then s -compound V in union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } by A2, TARSKI:def 4;

then s -compound V in (union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ) \/ ((S -termsOfMaxDepth) . mm) by XBOOLE_0:def 3;

then s -compound V in (S -termsOfMaxDepth) . (mm + 1) by FOMODEL1:def 30;

hence for b_{1} being string of S st b_{1} = s -compound V holds

b_{1} is mm + 1 -termal
; :: thesis: verum

end;then s -compound V in union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } by A2, TARSKI:def 4;

then s -compound V in (union { (Compound (u,((S -termsOfMaxDepth) . mm))) where u is ofAtomicFormula Element of S : u is operational } ) \/ ((S -termsOfMaxDepth) . mm) by XBOOLE_0:def 3;

then s -compound V in (S -termsOfMaxDepth) . (mm + 1) by FOMODEL1:def 30;

hence for b

b