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 b1 being object st b1 = [((H \/ {(<*l1*> ^ phi1)}) null l2),phi2] holds
b1 is 1,{[(H \/ {((l1,l2) -SymbolSubstIn phi1)}),phi2]},{(R#5 S)} -derivable
by Lm7; verum