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

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)

hence
IT = IT9
by BINOP_1:2; :: thesis: verumlet 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;thus IT . (u,v) = mi ((@ u) =>> (@ v)) by A5

.= IT9 . (u,v) by A6 ; :: thesis: verum