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