theorem Th3: :: FOMODEL1:3

for mm being Element of NAT
for S being Language
for w being b₁ + 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) )