set E = TheEqSymbOf S;
set AF = AllFormulasOf S;
reconsider phi0 = (<*(TheEqSymbOf S)*> ^ t1) ^ t2, phi1 = (<*(TheEqSymbOf S)*> ^ t) ^ t1, phi2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 as 0wff string of S by Lm10;
phi0 in AllFormulasOf S ;
then reconsider Phi0 = {phi0} as finite Subset of (AllFormulasOf S) by ZFMISC_1:31;
reconsider prem2 = premises \/ Phi0 as finite Subset of (AllFormulasOf S) ;
reconsider seqt2 = [prem2,phi2], seqt1 = [premises,phi1] as Element of S -sequents by DefSeqtLike;
reconsider Seqts = {seqt1} as Subset of (S -sequents) ;
B0: seqt1 in Seqts by TARSKI:def 1;
B1: seqt2 `1 = premises \/ {phi0} by MCART_1:7
.= (seqt1 `1) \/ {phi0} by MCART_1:7 ;
B2: ( seqt1 `2 = phi1 & seqt2 `2 = phi2 ) by MCART_1:7;
seqt2 Rule3a Seqts by B0, B1, B2, Def3a;
then [Seqts,seqt2] in P3a S by DefP3a;
hence for b₁ being set st b₁ = [(premises \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)}),((<*(TheEqSymbOf S)*> ^ t) ^ t2)] holds
b₁ is 1,{[premises,((<*(TheEqSymbOf S)*> ^ t) ^ t1)]},{(R3a S)} -derivable by Lm1b; :: thesis: verum