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

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

hence
IT = IT9
by FUNCT_2:63; :: thesis: verumlet 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;thus IT . u = mi (- (@ u)) by A2

.= IT9 . u by A3 ; :: thesis: verum