reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;

deffunc H_{1}( Element of AtomicFormulasOf S) -> string of S = (l,tt) AtomicSubst $1;

consider f being Function such that

A1: ( dom f = AtomicFormulasOf S & ( for x being Element of AtomicFormulasOf S holds f . x = H_{1}(x) ) )
from FUNCT_1:sch 4();

take ff ; :: thesis: for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

ff . phi0 = (l,tt) AtomicSubst phi0

deffunc H

consider f being Function such that

A1: ( dom f = AtomicFormulasOf S & ( for x being Element of AtomicFormulasOf S holds f . x = H

now :: thesis: for x being object st x in AtomicFormulasOf S holds

f . x in AtomicFormulasOf S

then reconsider ff = f as Function of (AtomicFormulasOf S),(AtomicFormulasOf S) by A1, FUNCT_2:3;f . x in AtomicFormulasOf S

let x be object ; :: thesis: ( x in AtomicFormulasOf S implies f . x in AtomicFormulasOf S )

assume x in AtomicFormulasOf S ; :: thesis: f . x in AtomicFormulasOf S

then reconsider tt = x as Element of AtomicFormulasOf S ;

f . tt = H_{1}(tt)
by A1;

then reconsider y = f . x as 0wff string of S ;

y in AtomicFormulasOf S ;

hence f . x in AtomicFormulasOf S ; :: thesis: verum

end;assume x in AtomicFormulasOf S ; :: thesis: f . x in AtomicFormulasOf S

then reconsider tt = x as Element of AtomicFormulasOf S ;

f . tt = H

then reconsider y = f . x as 0wff string of S ;

y in AtomicFormulasOf S ;

hence f . x in AtomicFormulasOf S ; :: thesis: verum

take ff ; :: thesis: for phi0 being 0wff string of S

for tt being Element of AllTermsOf S st tt = t holds

ff . phi0 = (l,tt) AtomicSubst phi0

hereby :: thesis: verum

let phi0 be 0wff string of S; :: thesis: for tt1 being Element of AllTermsOf S st tt1 = t holds

ff . phi0 = (l,tt1) AtomicSubst phi0

let tt1 be Element of AllTermsOf S; :: thesis: ( tt1 = t implies ff . phi0 = (l,tt1) AtomicSubst phi0 )

phi0 in AtomicFormulasOf S ;

then reconsider phi = phi0 as Element of AtomicFormulasOf S ;

assume tt1 = t ; :: thesis: ff . phi0 = (l,tt1) AtomicSubst phi0

then ( tt1 = tt & f . phi = (l,tt) AtomicSubst phi ) by A1;

hence ff . phi0 = (l,tt1) AtomicSubst phi0 ; :: thesis: verum

end;ff . phi0 = (l,tt1) AtomicSubst phi0

let tt1 be Element of AllTermsOf S; :: thesis: ( tt1 = t implies ff . phi0 = (l,tt1) AtomicSubst phi0 )

phi0 in AtomicFormulasOf S ;

then reconsider phi = phi0 as Element of AtomicFormulasOf S ;

assume tt1 = t ; :: thesis: ff . phi0 = (l,tt1) AtomicSubst phi0

then ( tt1 = tt & f . phi = (l,tt) AtomicSubst phi ) by A1;

hence ff . phi0 = (l,tt1) AtomicSubst phi0 ; :: thesis: verum