deffunc H₁( Element of SubstitutionSet V,C) -> Element of SubstitutionSet V,C = mi (- $1);
consider IT being Function of (SubstitutionSet V,C),(SubstitutionSet V,C) such that
A1: for u being Element of SubstitutionSet V,C holds IT . u = H₁(u) from FUNCT_2:sch 4();
SubstitutionSet V,C = the carrier of (SubstLatt V,C) by SUBSTLAT:def 4;
then reconsider IT = IT as UnOp of the carrier of (SubstLatt V,C) ;
take IT ; :: thesis: for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
IT . u = mi (- u9)
thus for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
IT . u = mi (- u9) by A1; :: thesis: verum