theorem Th16: :: FOMODEL1:16

for S being Language
for t being termal string of S st not t is 0 -termal holds
( (S -firstChar) . t is operational & SubTerms t <> {} )