set SS = AllSymbolsOf S;
set A = AllTermsOf S;
deffunc H₁( Element of AllTermsOf S) -> Element of (AllTermsOf S) * = SubTerms $1;
consider f being Function of (AllTermsOf S),((AllTermsOf S) *) 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 = SubTerms t
thus for t being Element of AllTermsOf S holds f . t = SubTerms t by A1; :: thesis: verum