let S be Language; :: thesis: for t1, t2 being termal string of S holds (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S
let t1, t2 be termal string of S; :: thesis: (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S
set E = TheEqSymbOf S;
set AT = AllTermsOf S;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
reconsider tt1 = t1, tt2 = t2 as Element of AllTermsOf S by Def32;
reconsider T = <*tt1*> ^ <*tt2*> as 2 -element Element of (AllTermsOf S) * ;
reconsider ATT = AllTermsOf S as Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1;
reconsider TT = T as Element of ATT * ;
reconsider TTT = TT as Element of ((AllSymbolsOf S) *) * ;
reconsider EE = TheEqSymbOf S as ofAtomicFormula Element of S ;
A1: |.(- 2).| = - (- 2) by ABSVALUE:def 1
.= 2 ;
A2: |.(ar EE).| = 2 by A1, Def23;
(S -multiCat) . TT is Element of (AllSymbolsOf S) * ;
then reconsider tailer = (S -multiCat) . T as FinSequence of AllSymbolsOf S ;
reconsider SSS = AllSymbolsOf S as non empty set ;
reconsider EEE = EE as Element of SSS ;
reconsider header = <*EEE*> as FinSequence of AllSymbolsOf S ;
reconsider IT = header ^ tailer as non empty FinSequence of AllSymbolsOf S ;
reconsider phi = IT as string of S by Th12;
tailer = ((AllSymbolsOf S) -multiCat) . <*tt1,tt2*>
.= tt1 ^ tt2 by FOMODEL0:15 ;
then ( phi = (<*(TheEqSymbOf S)*> ^ tt1) ^ tt2 & phi is 0wff string of S ) by A2, Def35, FINSEQ_1:32;
hence (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is 0wff string of S ; :: thesis: verum