let R be domRing; :: thesis: for S being domRingExtension of R
for n being non zero Element of NAT
for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let S be domRingExtension of R; :: thesis: for n being non zero Element of NAT
for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let n be non zero Element of NAT ; :: thesis: for a being Element of S holds Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let a be Element of S; :: thesis: Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
reconsider q = <%(0. S),(1. S)%> `^ n as Element of the carrier of (Polynom-Ring S) by POLYNOM3:def 10;
reconsider p = <%(0. R),(1. R)%> `^ n as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
R is Subring of S by FIELD_4:def 1;
then ( 0. R = 0. S & 1. R = 1. S ) by C0SP1:def 3;
then <%(0. R),(1. R)%> `^ n = <%(0. S),(1. S)%> `^ n by helpp;
then Ext_eval (p,a) = eval (q,a) by FIELD_4:26
.= a |^ n by help3a ;
hence Ext_eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n ; :: thesis: verum