let S be Language; :: thesis: for t being termal string of S st not t is 0 -termal holds
( (S -firstChar) . t is operational & SubTerms t <> {} )
let t be termal string of S; :: thesis: ( not t is 0 -termal implies ( (S -firstChar) . t is operational & SubTerms t <> {} ) )
set T = S -termsOfMaxDepth ;
set m = Depth t;
set ST = SubTerms t;
set TT = AllTermsOf S;
assume not t is 0 -termal ; :: thesis: ( (S -firstChar) . t is operational & SubTerms t <> {} )
then Depth t <> 0 by DefDepth2;
then consider n being Nat such that
B0: Depth t = n + 1 by NAT_1:6;
set F = S -firstChar ;
set C = S -multiCat ;
set Fam = { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ;
n < Depth t by B0, NAT_1:16;
then ( not t is n -termal & t is Depth t -termal ) by DefDepth2;
then ( not t in (S -termsOfMaxDepth) . n & t in (S -termsOfMaxDepth) . (n + 1) ) by B0, DefTermal;
then ( t in (union { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ ((S -termsOfMaxDepth) . n) & not t in (S -termsOfMaxDepth) . n ) by DefTerm;
then t in union { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } by XBOOLE_0:def 3;
then consider x being set such that
B1: ( t in x & x in { (Compound (s,((S -termsOfMaxDepth) . n))) where s is ofAtomicFormula Element of S : s is operational } ) by TARSKI:def 4;
consider s being ofAtomicFormula Element of S such that
B2: ( x = Compound (s,((S -termsOfMaxDepth) . n)) & s is operational ) by B1;
set k = abs (ar s);
consider StringTuple being Element of ((AllSymbolsOf S) *) * such that
B3: ( t = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . n & StringTuple is abs (ar s) -element ) by B1, B2;
B4: (S -firstChar) . t = (<*s*> ^ ((S -multiCat) . StringTuple)) . 1 by B3, FOMODEL0:6
.= <*s*> . 1 by FOMODEL0:28
.= s by FINSEQ_1:40 ;
hence (S -firstChar) . t is operational by B2; :: thesis: SubTerms t <> {}
reconsider k1 = abs (ar s) as non zero Nat by B2;
reconsider STT = SubTerms t as k1 + 0 -element Element of (AllTermsOf S) * by B4;
STT <> {} ;
hence SubTerms t <> {} ; :: thesis: verum