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 :: thesis: for u being Element of (SubstLatt (V,C)) holds IT . u = IT9 . u
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:63; :: thesis: verum