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

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