let a, b be Element of multEX_0; :: thesis: a * b = b * a
reconsider p = a, q = b as Real ;
thus a * b = q * p by BINOP_2:def 11
.= b * a by BINOP_2:def 11 ; :: thesis: verum