take multEX_0 ; :: thesis: multEX_0 is right_unital
thus multEX_0 is right_unital ; :: thesis: verum