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;
B2: 2 -tuples_on (AllTermsOf S) = { <*tt1,tt2*> where tt1, tt2 is Element of AllTermsOf S : verum } by FINSEQ_2:99;
B0: ( phi0 = <*(TheEqSymbOf S)*> ^ (t1 ^ t2) & ((<*(TheEqSymbOf S)*> ^ (t1 ^ t2)) . 1) \+\ (TheEqSymbOf S) = {} ) by FINSEQ_1:32;
then B1: 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 B0, FOMODEL1:def 38;
then B4: (S -multiCat) . (SubTerms phi0) = t1 ^ t2 by FOMODEL0:41;
((abs (ar (TheEqSymbOf S))) - 2) + 2 = 0 + 2 ;
then SubTerms phi0 in 2 -tuples_on (AllTermsOf S) by B1, FOMODEL0:16;
then consider tt1, tt2 being Element of AllTermsOf S such that
B3: SubTerms phi0 = <*tt1,tt2*> by B2;
( 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 B3, B4, FOMODEL0:29;
then ( tt11 = tt33 & tt22 = tt44 ) by FOMODEL0:def 20;
hence for b₁ being set st b₁ = (SubTerms ((<*(TheEqSymbOf S)*> ^ t1) ^ t2)) \+\ <*t1,t2*> holds
b₁ is empty by B3, FOMODEL0:29; :: thesis: verum