let R be non empty non degenerated well-unital doubleLoopStr ; for a being Element of R holds <%(- a),(1. R)%> = rpoly (1,a)
let a be Element of R; <%(- a),(1. R)%> = rpoly (1,a)
set p = <%(- a),(1. R)%>;
set q = rpoly (1,a);
A: 1 =
deg (rpoly (1,a))
by HURWITZ:27
.=
(len (rpoly (1,a))) - 1
by HURWITZ:def 2
;
D:
1. R <> 0. R
;
hence
<%(- a),(1. R)%> = rpoly (1,a)
by A, D, POLYNOM5:40, ALGSEQ_1:12; verum