let IT, IT' 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 IT' . u = mi (- (@ u)) ) implies IT = IT' )
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 IT' . u = mi (- (@ u)) ; :: thesis: IT = IT'

now

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

end;

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