let R be non empty non degenerated well-unital doubleLoopStr ; :: thesis: for a being Element of R holds <%(- a),(1. R)%> = rpoly (1,a)
let a be Element of R; :: thesis: <%(- 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 ;
now :: thesis: for k being Nat st k < len <%(- a),(1. R)%> holds
<%(- a),(1. R)%> . k = (rpoly (1,a)) . k
let k be Nat; :: thesis: ( k < len <%(- a),(1. R)%> implies <%(- a),(1. R)%> . b1 = (rpoly (1,a)) . b1 )
assume k < len <%(- a),(1. R)%> ; :: thesis: <%(- a),(1. R)%> . b1 = (rpoly (1,a)) . b1
then k < 1 + 1 by D, POLYNOM5:40;
then B: k <= 1 by NAT_1:13;
per cases ( k = 0 or k = 1 ) by B, NAT_1:25;
suppose C: k = 0 ; :: thesis: <%(- a),(1. R)%> . b1 = (rpoly (1,a)) . b1
hence <%(- a),(1. R)%> . k = - ((1_ R) * a) by POLYNOM5:38
.= - (((power R) . (a,0)) * a) by GROUP_1:def 7
.= - ((power R) . (a,(0 + 1))) by GROUP_1:def 7
.= (rpoly (1,a)) . k by C, HURWITZ:25 ;
:: thesis: verum
end;
suppose C: k = 1 ; :: thesis: <%(- a),(1. R)%> . b1 = (rpoly (1,a)) . b1
hence <%(- a),(1. R)%> . k = 1_ R by POLYNOM5:38
.= (rpoly (1,a)) . k by C, HURWITZ:25 ;
:: thesis: verum
end;
end;
end;
hence <%(- a),(1. R)%> = rpoly (1,a) by A, D, POLYNOM5:40, ALGSEQ_1:12; :: thesis: verum