let S be Language; :: thesis: for s being Element of S
for w being string of S holds
( s is {w} -occurring iff s in rng w )
let s be Element of S; :: thesis: for w being string of S holds
( s is {w} -occurring iff s in rng w )
let w be string of S; :: thesis: ( s is {w} -occurring iff s in rng w )
set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
reconsider X = {w} as non empty Subset of (((AllSymbolsOf S) *) \ {{}}) ;
SymbolsOf ((((AllSymbolsOf S) *) \ {{}}) /\ X) = rng w by FOMODEL0:45;
hence ( s is {w} -occurring iff s in rng w ) by Def38; :: thesis: verum