set LH = (l,tt) SubstIn phi0;
set RH = (l,tt) AtomicSubst phi0;
set f1 = l Subst1 tt;
set f4 = (l,tt) Subst4 (l Subst1 tt);
set f0 = l AtomicSubst tt;
set AF = AtomicFormulasOf S;
( phi0 in AtomicFormulasOf S & dom (l AtomicSubst tt) = AtomicFormulasOf S ) by FUNCT_2:def 1;
then reconsider phi00 = phi0 as Element of dom (l AtomicSubst tt) ;
thus (l,tt) SubstIn phi0 = (l Subst1 tt) . phi00 by Def22
.= (l AtomicSubst tt) . phi00 by FUNCT_4:13
.= (l,tt) AtomicSubst phi0 by Def23 ; :: thesis: verum