theorem :: FOMODEL2:1

for S being Language
for t0 being 0 -termal string of S holds t0 = <*((S -firstChar) . t0)*>