reconsider tt = t as Element of AllTermsOf S by FOMODEL1:def 32;
deffunc H1( 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 = H1(x) ) ) from FUNCT_1:sch 4();
now :: thesis: for x being object st x in AtomicFormulasOf S holds
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 = H1(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;
then reconsider ff = f as Function of (AtomicFormulasOf S),(AtomicFormulasOf S) by A1, FUNCT_2:3;
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;