set E = TheEqSymbOf S;
set TT = AllTermsOf S;
deffunc H₁( Element of AllTermsOf S) -> Element of ((AllSymbolsOf S) *) \ {{}} = (<*(TheEqSymbOf S)*> ^ $1) ^ $1;
defpred S₁[ set ] means verum;
set IT = { [tt,H₁(tt)] where tt is Element of AllTermsOf S : S₁[tt] } ;
{ [tt,H₁(tt)] where tt is Element of AllTermsOf S : S₁[tt] } is Function from ALTCAT_2:sch 1();
hence { [tt,((<*(TheEqSymbOf S)*> ^ tt) ^ tt)] where tt is Element of AllTermsOf S : verum } is Function ; :: thesis: verum