reconsider phi11 = (l1,l2) -SymbolSubstIn phi1 as wff string of S ;
set H1 = H \/ {phi11};
set Sq1 = [(H \/ {phi11}),phi2];
set H2 = H \/ {(<*l1*> ^ phi1)};
set Sq2 = [(H \/ {(<*l1*> ^ phi1)}),phi2];
set R = R#5 S;
set Q = S -sequents ;
set x = H;
set SS = AllSymbolsOf S;
set SQ = {[(H \/ {phi11}),phi2]};
set s = l1 SubstWith l2;
reconsider p = phi1 as AllSymbolsOf S -valued FinSequence ;
reconsider seqt = [(H \/ {(<*l1*> ^ phi1)}),phi2] as Element of S -sequents by Def2;
reconsider Seqts = {[(H \/ {phi11}),phi2]} as Element of bool (S -sequents) by Def3;
H \/ {((l1 SubstWith l2) . p)} = H \/ {phi11} by FOMODEL0:def 22;
then [(H \/ {((l1 SubstWith l2) . p)}),(seqt `2)] in Seqts by TARSKI:def 1;
then seqt Rule5 Seqts ;
then [Seqts,seqt] in P#5 S by Def42;
then seqt in (R#5 S) . Seqts by Th3;
hence for b₁ being object st b₁ = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds
b₁ is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R#5 S)} -derivable by Lm7; :: thesis: verum