let IT, IT9 be BinOp of the carrier of (NormForm A); :: thesis: ( ( for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v)) ) & ( for u, v being Element of (NormForm A) holds IT9 . (u,v) = mi ((@ u) =>> (@ v)) ) implies IT = IT9 )
assume that
A5: for u, v being Element of (NormForm A) holds IT . (u,v) = mi ((@ u) =>> (@ v)) and
A6: for u, v being Element of (NormForm A) holds IT9 . (u,v) = mi ((@ u) =>> (@ v)) ; :: thesis: IT = IT9

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

let u, v be Element of (NormForm A); :: thesis: IT . (u,v) = IT9 . (u,v)
thus IT . (u,v) = mi ((@ u) =>> (@ v)) by A5
.= IT9 . (u,v) by A6 ; :: thesis: verum

end;

hence IT = IT9 by BINOP_1:2; :: thesis: verum