let S be Language; for l being literal Element of S
for phi0 being 0wff string of S
for tt being Element of AllTermsOf S holds
( (S -firstChar) . ((l,tt) AtomicSubst phi0) = (S -firstChar) . phi0 & SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0) )
let l be literal Element of S; for phi0 being 0wff string of S
for tt being Element of AllTermsOf S holds
( (S -firstChar) . ((l,tt) AtomicSubst phi0) = (S -firstChar) . phi0 & SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0) )
let phi0 be 0wff string of S; for tt being Element of AllTermsOf S holds
( (S -firstChar) . ((l,tt) AtomicSubst phi0) = (S -firstChar) . phi0 & SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0) )
let tt be Element of AllTermsOf S; ( (S -firstChar) . ((l,tt) AtomicSubst phi0) = (S -firstChar) . phi0 & SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0) )
set psi0 = (l,tt) AtomicSubst phi0;
set F = S -firstChar ;
set C = S -multiCat ;
set TT = AllTermsOf S;
set FI = (S,{}) -freeInterpreter ;
set I = (l,tt) ReassignIn ((S,{}) -freeInterpreter);
set s1 = (S -firstChar) . phi0;
set s2 = (S -firstChar) . ((l,tt) AtomicSubst phi0);
set n1 = |.(ar ((S -firstChar) . phi0)).|;
set n2 = |.(ar ((S -firstChar) . ((l,tt) AtomicSubst phi0))).|;
thus A1: (S -firstChar) . ((l,tt) AtomicSubst phi0) =
((l,tt) AtomicSubst phi0) . 1
by FOMODEL0:6
.=
(S -firstChar) . phi0
by FINSEQ_1:41
; SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)
reconsider ST = SubTerms phi0 as |.(ar ((S -firstChar) . phi0)).| -element FinSequence of AllTermsOf S by FOMODEL0:26;
reconsider newST = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * ST as |.(ar ((S -firstChar) . ((l,tt) AtomicSubst phi0))).| -element FinSequence of AllTermsOf S by A1;
newST = SubTerms ((l,tt) AtomicSubst phi0)
by A1, FOMODEL1:def 38;
hence
SubTerms ((l,tt) AtomicSubst phi0) = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * (SubTerms phi0)
; verum