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

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