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 ) )