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)) . b1 = (rpoly (n,(0. R))) . b1
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)) . b1 = (rpoly (n,(0. R))) . b1
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)) . b1 = (rpoly (n,(0. R))) . b1
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)) . b1 = (rpoly (n,(0. R))) . b1
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