:: deftheorem defines pmult QUOFIELD:def 3 :
for I being non empty non degenerated domRing-like doubleLoopStr
for u, v being Element of Q. I holds pmult (u,v) = [((u `1) * (v `1)),((u `2) * (v `2))];