theorem Th13: :: FIELD_1:12

for n being Nat
for R being non degenerated comRing holds <%(0. R),(1. R)%> `^ n = anpoly ((1. R),n)