let IT, IT9 be UnOp of the carrier of (NormForm A); :: thesis: ( ( for u being Element of (NormForm A) holds IT . u = mi (- (@ u)) ) & ( for u being Element of (NormForm A) holds IT9 . u = mi (- (@ u)) ) implies IT = IT9 )
assume that
A2: for u being Element of (NormForm A) holds IT . u = mi (- (@ u)) and
A3: for u being Element of (NormForm A) holds IT9 . u = mi (- (@ u)) ; :: thesis: IT = IT9

now :: thesis: for u being Element of (NormForm A) holds IT . u = IT9 . u

let u be Element of (NormForm A); :: thesis: IT . u = IT9 . u
thus IT . u = mi (- (@ u)) by A2
.= IT9 . u by A3 ; :: thesis: verum

end;

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