theorem Th1: :: MONOID_0:1

for D being non empty set
for f being BinOp of D holds
( f is invertible iff ( f is left-invertible & f is right-invertible ) )