(x,s) -SymbolSubstIn (w null w) is (len w) + 0 -element ;
hence (x,s) -SymbolSubstIn w is string of S by FOMODEL0:30; :: thesis: verum