set L1 = LettersOf S1;
set S2 = S1 addLettersNotIn X;
set no = SymbolsOf X;
set L2 = LettersOf (S1 addLettersNotIn X);
set IT = (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X);
set a1 = the adicity of S1;
set a2 = the adicity of (S1 addLettersNotIn X);
set SS1 = AllSymbolsOf S1;
set fresh = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ;
reconsider f = (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) --> 0 as INT -valued Function ;
A1: ( 0 in {0} & dom ((((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) --> 0) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ) by TARSKI:def 1;
(((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) /\ ((AllSymbolsOf S1) \/ (SymbolsOf X)) = {} ;
then ( ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet misses (AllSymbolsOf S1) null (SymbolsOf X) & ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet misses (SymbolsOf X) null (AllSymbolsOf S1) ) by XBOOLE_1:63, XBOOLE_0:def 7;
then A2: ( (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \ (AllSymbolsOf S1) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet & (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \ (SymbolsOf X) = ((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet ) by XBOOLE_1:83;
LettersOf (S1 addLettersNotIn X) = ((f | ((dom f) \ (AllSymbolsOf S1))) " {0}) \/ (LettersOf S1) by Lm12;
then (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) = ((((f null {}) | ({} \/ (dom f))) " {0}) \ (SymbolsOf X)) \/ ((LettersOf S1) \ (SymbolsOf X)) by XBOOLE_1:42, A2
.= (((AllSymbolsOf S1) \/ (SymbolsOf X)) -freeCountableSet) \/ ((LettersOf S1) \ (SymbolsOf X)) by FUNCOP_1:14, A1, A2 ;
hence for b₁ being set st b₁ = (LettersOf (S1 addLettersNotIn X)) \ (SymbolsOf X) holds
not b₁ is finite ; :: thesis: verum