let IT, IT' be UnOp of the carrier of (SubstLatt V,C); :: thesis: ( ( for u being Element of
for u' being Element of SubstitutionSet V,C st u' = u holds
IT . u = mi (- u') ) & ( for u being Element of
for u' being Element of SubstitutionSet V,C st u' = u holds
IT' . u = mi (- u') ) implies IT = IT' )
assume that
A2: for u being Element of
for u' being Element of SubstitutionSet V,C st u' = u holds
IT . u = mi (- u') and
A3: for u being Element of
for u' being Element of SubstitutionSet V,C st u' = u holds
IT' . u = mi (- u') ; :: thesis: IT = IT'

now

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

end;

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