Description: Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019)