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 u' being Element of SubstitutionSet V,C st u' = u holds
IT . u = mi (- u')
thus for u being Element of (SubstLatt V,C)
for u' being Element of SubstitutionSet V,C st u' = u holds
IT . u = mi (- u') by A1; :: thesis: verum