let S be Language; :: thesis: for t0 being 0 -termal string of S holds t0 = <*((S -firstChar) . t0)*>
let t0 be 0 -termal string of S; :: thesis: t0 = <*((S -firstChar) . t0)*>
reconsider e = (S -multiCat) . (SubTerms t0) as empty set ;
t0 = <*((S -firstChar) . t0)*> ^ e by FOMODEL1:def 37
.= <*((S -firstChar) . t0)*> ;
hence t0 = <*((S -firstChar) . t0)*> ; :: thesis: verum