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