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

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

hence
IT1 = IT2
by FUNCT_2:63; :: thesis: verumlet 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;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