set SS = AllSymbolsOf S;
reconsider w11 = w1, w22 = w2 as non empty FinSequence of AllSymbolsOf S by FOMODEL0:5;
w11 ^ w22 is non empty FinSequence of AllSymbolsOf S ;
hence w1 ^ w2 is string of S by FOMODEL0:5; :: thesis: verum