let A, B be Ring; :: thesis: 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)
let n be Nat; :: thesis: 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)
let x be Element of A; :: thesis: 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)
let p be Polynomial of A; :: thesis: ( A is Subring of B implies (In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B) )
assume A0: A is Subring of B ; :: thesis: (In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B)
then In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B) = (In ((p . (n -' 1)),B)) * (In (((power A) . (x,(n -' 1))),B)) by Th13
.= (In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) by A0, Th11 ;
hence (In ((p . (n -' 1)),B)) * ((power B) . ((In (x,B)),(n -' 1))) = In (((p . (n -' 1)) * ((power A) . (x,(n -' 1)))),B) ; :: thesis: verum