take multMagma(# {}, the BinOp of {} #) ; :: thesis: multMagma(# {}, the BinOp of {} #) is empty
thus multMagma(# {}, the BinOp of {} #) is empty ; :: thesis: verum