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 (l,tt) AtomicSubst phi0 is 0wff string of S
let l be literal Element of S; :: thesis: for phi0 being 0wff string of S
for tt being Element of AllTermsOf S holds (l,tt) AtomicSubst phi0 is 0wff string of S
let phi0 be 0wff string of S; :: thesis: for tt being Element of AllTermsOf S holds (l,tt) AtomicSubst phi0 is 0wff string of S
let tt be Element of AllTermsOf S; :: thesis: (l,tt) AtomicSubst phi0 is 0wff string of S
set ST = SubTerms phi0;
set FI = (S,{}) -freeInterpreter ;
set I = (l,tt) ReassignIn ((S,{}) -freeInterpreter);
set C = S -multiCat ;
set F = S -firstChar ;
set r = (S -firstChar) . phi0;
set n = |.(ar ((S -firstChar) . phi0)).|;
set TT = AllTermsOf S;
set TE = ((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval ;
set SS = AllSymbolsOf S;
reconsider STT = SubTerms phi0 as FinSequence of AllTermsOf S by FOMODEL0:26;
reconsider newterms = (((l,tt) ReassignIn ((S,{}) -freeInterpreter)) -TermEval) * STT as FinSequence of AllTermsOf S ;
reconsider newtermss = newterms as Element of ((AllSymbolsOf S) *) * by TARSKI:def 3;
reconsider IT = <*((S -firstChar) . phi0)*> ^ ((S -multiCat) . newtermss) as string of S by FOMODEL0:30;
IT is 0wff ;
hence (l,tt) AtomicSubst phi0 is 0wff string of S ; :: thesis: verum