let n be Nat; for R being non degenerated comRing
for a, b being non zero Element of R holds b * (anpoly (a,n)) = anpoly ((a * b),n)
let R be non degenerated comRing; for a, b being non zero Element of R holds b * (anpoly (a,n)) = anpoly ((a * b),n)
let a, b be non zero Element of R; b * (anpoly (a,n)) = anpoly ((a * b),n)
hence
b * (anpoly (a,n)) = anpoly ((a * b),n)
; verum