reconsider o = rpoly (1,(1. R)) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
take o ; :: thesis: o is linear
thus o is linear by HURWITZ:27; :: thesis: verum