let mm be Element of NAT ; :: thesis: for S being Language
for w being mm + 1 -termal string of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
let S be Language; :: thesis: for w being mm + 1 -termal string of S ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
let w be mm + 1 -termal string of S; :: thesis: ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) )
consider s being termal Element of S, T being Element of ((S -termsOfMaxDepth) . mm) * such that
A1: ( T is |.(ar s).| -element & w = <*s*> ^ ((S -multiCat) . T) ) by Lm8;
reconsider ww = w as non empty FinSequence of AllSymbolsOf S by FINSEQ_1:def 11;
s = w . 1 by A1, FINSEQ_1:41
.= (S -firstChar) . w by FOMODEL0:6 ;
hence ex T being Element of ((S -termsOfMaxDepth) . mm) * st
( T is |.(ar ((S -firstChar) . w)).| -element & w = <*((S -firstChar) . w)*> ^ ((S -multiCat) . T) ) by A1; :: thesis: verum