theorem Th3: :: MONOID_0:3

for x being set
for f being BinOp of {x} holds
( f = (x,x) .--> x & f is having_a_unity & f is commutative & f is associative & f is idempotent & f is invertible & f is cancelable & f is uniquely-decomposable )