let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: b * (anpoly (a,n)) = anpoly ((a * b),n)

now :: thesis: for i being Element of NAT holds (b * (anpoly (a,n))) . i = (anpoly ((a * b),n)) . i

let i be Element of NAT ; :: thesis: (b * (anpoly (a,n))) . b₁ = (anpoly ((a * b),n)) . b₁
set p = anpoly (a,n);
set q = anpoly ((a * b),n);

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

suppose A1: i = n ; :: thesis: (b * (anpoly (a,n))) . b₁ = (anpoly ((a * b),n)) . b₁

(b * (anpoly (a,n))) . i = b * ((anpoly (a,n)) . i) by POLYNOM5:def 4
.= b * a by A1, POLYDIFF:24
.= (anpoly ((a * b),n)) . i by A1, POLYDIFF:24 ;
hence (b * (anpoly (a,n))) . i = (anpoly ((a * b),n)) . i ; :: thesis: verum

end;

suppose A2: i <> n ; :: thesis: (b * (anpoly (a,n))) . b₁ = (anpoly ((a * b),n)) . b₁

(b * (anpoly (a,n))) . i = b * ((anpoly (a,n)) . i) by POLYNOM5:def 4
.= b * (0. R) by A2, POLYDIFF:25
.= (anpoly ((a * b),n)) . i by A2, POLYDIFF:25 ;
hence (b * (anpoly (a,n))) . i = (anpoly ((a * b),n)) . i ; :: thesis: verum

end;

end;

end;

hence b * (anpoly (a,n)) = anpoly ((a * b),n) ; :: thesis: verum