let S be Language; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: 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) ; :: thesis: verum