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
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: IT1 = IT2

now :: thesis: for x being Element of AtomicFormulasOf S holds IT1 . x = IT2 . x

let x be Element of AtomicFormulasOf S; :: thesis: IT1 . x = IT2 . x
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: verum

end;

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