let IT, IT9 be UnOp of the carrier of (SubstLatt V,C); :: 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) ) & ( for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
IT9 . u = mi (- u9) ) implies IT = IT9 )
assume that
A2: for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
IT . u = mi (- u9) and
A3: for u being Element of (SubstLatt V,C)
for u9 being Element of SubstitutionSet V,C st u9 = u holds
IT9 . u = mi (- u9) ; :: thesis: IT = IT9

now

let u be Element of (SubstLatt V,C); :: thesis: IT . u = IT9 . u
reconsider u9 = u as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
thus IT . u = mi (- u9) by A2
.= IT9 . u by A3 ; :: thesis: verum

end;

hence IT = IT9 by FUNCT_2:113; :: thesis: verum