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