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

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