let IT, IT9 be UnOp of the carrier of (NormForm A); :: thesis: ( ( for v being Element of (NormForm A) holds IT . v = u \ v ) & ( for v being Element of (NormForm A) holds IT9 . v = u \ v ) implies IT = IT9 )
assume that
A9: for v being Element of (NormForm A) holds IT . v = u \ v and
A10: for v being Element of (NormForm A) holds IT9 . v = u \ v ; :: thesis: IT = IT9

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

let v be Element of (NormForm A); :: thesis: IT . v = IT9 . v
thus IT . v = u \ v by A9
.= IT9 . v by A10 ; :: thesis: verum

end;

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