let R be non degenerated Ring; :: thesis: for n being non zero Element of NAT holds anpoly ((1. R),n) = rpoly (n,(0. R))
let n be non zero Element of NAT ; :: thesis: anpoly ((1. R),n) = rpoly (n,(0. R))
set p = anpoly ((1. R),n);
set r = rpoly (n,(0. R));

now :: thesis: for i being Element of NAT holds (anpoly ((1. R),n)) . i = (rpoly (n,(0. R))) . i

let i be Element of NAT ; :: thesis: (anpoly ((1. R),n)) . b₁ = (rpoly (n,(0. R))) . b₁
A1: 1 <= n by NAT_1:53;

per cases ( i = 0 or i = n or ( i <> 0 & i <> n ) ) ;

suppose A2: i = 0 ; :: thesis: (anpoly ((1. R),n)) . b₁ = (rpoly (n,(0. R))) . b₁

then (rpoly (n,(0. R))) . i = - ((power R) . ((0. R),n)) by HURWITZ:25
.= - ((0. R) |^ n) by BINOM:def 2
.= - (0. R) by A1, EC_PF_2:5
.= (anpoly ((1. R),n)) . i by A2, POLYDIFF:25 ;
hence (anpoly ((1. R),n)) . i = (rpoly (n,(0. R))) . i ; :: thesis: verum

end;

suppose A3: i = n ; :: thesis: (anpoly ((1. R),n)) . b₁ = (rpoly (n,(0. R))) . b₁

then (rpoly (n,(0. R))) . i = 1_ R by HURWITZ:25
.= (anpoly ((1. R),n)) . i by A3, POLYDIFF:24 ;
hence (anpoly ((1. R),n)) . i = (rpoly (n,(0. R))) . i ; :: thesis: verum

end;

suppose A4: ( i <> 0 & i <> n ) ; :: thesis: (anpoly ((1. R),n)) . b₁ = (rpoly (n,(0. R))) . b₁

then (rpoly (n,(0. R))) . i = 0. R by HURWITZ:26
.= (anpoly ((1. R),n)) . i by A4, POLYDIFF:25 ;
hence (anpoly ((1. R),n)) . i = (rpoly (n,(0. R))) . i ; :: thesis: verum

end;

end;

end;

hence anpoly ((1. R),n) = rpoly (n,(0. R)) ; :: thesis: verum