let u, v be Element of Q. I; :: thesis: pmult (u,v) = pmult (v,u)
thus pmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))]
.= pmult (v,u) ; :: thesis: verum