let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R
for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)
let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R
for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for a being Element of R
for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)
let a be Element of R; :: thesis: for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)
let b be Element of S; :: thesis: ( b = a implies Ext_eval (p,b) = eval (p,a) )
assume A1: b = a ; :: thesis: Ext_eval (p,b) = eval (p,a)
A2: R is Subring of S by FIELD_4:def 1;
then A3: the carrier of R c= the carrier of S by C0SP1:def 3;
Ext_eval (p,(In (a,S))) = In ((eval (p,a)),S) by A2, ALGNUM_1:12
.= eval (p,a) by A3, SUBSET_1:def 8 ;
hence Ext_eval (p,b) = eval (p,a) by A1; :: thesis: verum