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

now

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

end;

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