reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
let IT1, IT2 be Function of (AtomicFormulasOf S),(AtomicFormulasOf S); :: thesis: ( ( for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
IT1 . phi0 = (l,tt) AtomicSubst phi0 ) & ( for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
IT2 . phi0 = (l,tt) AtomicSubst phi0 ) implies IT1 = IT2 )
assume that
B1: for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
IT1 . phi0 = (l,tt) AtomicSubst phi0 and
B2: for phi0 being 0wff string of S
for tt being Element of AllTermsOf S st tt = t holds
IT2 . phi0 = (l,tt) AtomicSubst phi0 ; :: thesis: IT1 = IT2

now

let x be Element of AtomicFormulasOf S; :: thesis: IT1 . x = IT2 . x
consider w being string of S such that
C0: ( x = w & w is 0wff ) ;
reconsider phi0 = w as 0wff string of S by C0;
IT1 . phi0 = (l,tt) AtomicSubst phi0 by B1
.= IT2 . phi0 by B2 ;
hence IT1 . x = IT2 . x by C0; :: thesis: verum

end;

hence IT1 = IT2 by FUNCT_2:63; :: thesis: verum