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 Def1;

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

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 Def1;

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