set E = TheEqSymbOf S;
reconsider phi0 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2 as 0wff string of S ;
set C = S -multiCat ;
set F = S -firstChar ;
set ST = SubTerms phi0;
set SS = AllSymbolsOf S;
set TT = AllTermsOf S;
reconsider tt3 = t1, tt4 = t2 as Element of AllTermsOf S by FOMODEL1:def 32;
A1: 2 -tuples_on (AllTermsOf S) = { <*tt1,tt2*> where tt1, tt2 is Element of AllTermsOf S : verum } by FINSEQ_2:99;
A2: ( phi0 = <*(TheEqSymbOf S)*> ^ (t1 ^ t2) & ((<*(TheEqSymbOf S)*> ^ (t1 ^ t2)) . 1) \+\ (TheEqSymbOf S) = {} ) by FINSEQ_1:32;
then A3: TheEqSymbOf S = phi0 . 1 by FOMODEL0:29
.= (S -firstChar) . phi0 by FOMODEL0:6 ;
then <*(TheEqSymbOf S)*> ^ ((S -multiCat) . (SubTerms phi0)) = <*(TheEqSymbOf S)*> ^ (t1 ^ t2) by FOMODEL1:def 38, A2;
then A4: (S -multiCat) . (SubTerms phi0) = t1 ^ t2 by FOMODEL0:41;
(|.(ar (TheEqSymbOf S)).| - 2) + 2 = 0 + 2 ;
then SubTerms phi0 in 2 -tuples_on (AllTermsOf S) by FOMODEL0:16, A3;
then consider tt1, tt2 being Element of AllTermsOf S such that
A5: SubTerms phi0 = <*tt1,tt2*> by A1;
( tt1 is Element of (AllSymbolsOf S) * & tt2 is Element of (AllSymbolsOf S) * & tt3 is Element of (AllSymbolsOf S) * & tt4 is Element of (AllSymbolsOf S) * ) by TARSKI:def 3;
then reconsider tt11 = tt1, tt22 = tt2, tt33 = tt3, tt44 = tt4 as AllSymbolsOf S -valued FinSequence ;
((S -multiCat) . <*tt11,tt22*>) \+\ (tt11 ^ tt22) = {} ;
then tt11 ^ tt22 = tt33 ^ tt44 by FOMODEL0:29, A5, A4;
then ( tt11 = tt33 & tt22 = tt44 ) by FOMODEL0:def 19;
hence for b₁ being set st b₁ = (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> holds
b₁ is empty by FOMODEL0:29, A5; :: thesis: verum