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 Def40;
then consider n being Nat such that
A1: 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 A1, NAT_1:16;
then ( not t is n -termal & t is Depth t -termal ) by Def40;
then ( not t in (S -termsOfMaxDepth) . n & t in (S -termsOfMaxDepth) . (n + 1) ) by A1;
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 Def30;
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
A2: ( 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
A3: ( x = Compound (s,((S -termsOfMaxDepth) . n)) & s is operational ) by A2;
set k = |.(ar s).|;
consider StringTuple being Element of ((AllSymbolsOf S) *) * such that
A4: ( t = <*s*> ^ ((S -multiCat) . StringTuple) & rng StringTuple c= (S -termsOfMaxDepth) . n & StringTuple is |.(ar s).| -element ) by A2, A3;
A5: (S -firstChar) . t = (<*s*> ^ ((S -multiCat) . StringTuple)) . 1 by FOMODEL0:6, A4
.= <*s*> . 1 by FOMODEL0:28
.= s ;
hence (S -firstChar) . t is operational by A3; :: thesis: SubTerms t <> {}
reconsider k1 = |.(ar s).| as non zero Nat by A3;
reconsider STT = SubTerms t as k1 + 0 -element Element of (AllTermsOf S) * by A5;
STT <> {} ;
hence SubTerms t <> {} ; :: thesis: verum