reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
let IT1, IT2 be Function of (AtomicFormulasOf S),(AtomicFormulasOf S); :: thesis:
assume that
A2: 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
A3: 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:

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

end;