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