set A = AllTermsOf S;

deffunc H_{1}( 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_{1}(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

deffunc H

consider f being Function of (AllTermsOf S),U such that

A1: for t being Element of AllTermsOf S holds f . t = H

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