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