take rpoly (1,(0. R)) ; :: thesis: rpoly (1,(0. R)) is linear
thus rpoly (1,(0. R)) is linear by HURWITZ:27; :: thesis: verum