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

now

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

end;

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