theorem Th11: :: FIELD_1:10

for R being non degenerated comRing
for a, b being non zero Element of R
for n, m being Nat holds (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))