for A, B being Ring
for n being Nat
for x being Element of A
for p being Polynomial of A st A is Subring of B holds
(In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B)