set A = AllTermsOf S;
deffunc H₁( Element of AllTermsOf S) -> Element of U = I -TermEval $1;
consider f being Function of (AllTermsOf S),U such that
A1: for t being Element of AllTermsOf S holds f . t = H₁(t) from FUNCT_2:sch 4();
take f ; :: thesis: for t being Element of AllTermsOf S holds f . t = I -TermEval t
thus for t being Element of AllTermsOf S holds f . t = I -TermEval t by A1; :: thesis: verum