:: deftheorem defines addLettersNotIn FOMODEL1:def 43 :
for S being Language
for X being functional set holds S addLettersNotIn X = S extendWith ((((AllSymbolsOf S) \/ (SymbolsOf X)) -freeCountableSet) --> 0);