let R be Ring; :: thesis: for x being Element of R
for p being Polynomial of R holds Ext_eval (p,x) = eval (p,x)
let x be Element of R; :: thesis: for p being Polynomial of R holds Ext_eval (p,x) = eval (p,x)
let p be Polynomial of R; :: thesis: Ext_eval (p,x) = eval (p,x)
A1: ( 1. R = 1. R & 0. R = 0. R ) ;
A2: the addF of R = the addF of R | [: the carrier of R, the carrier of R:]
.= the addF of R || the carrier of R by REALSET1:def 2 ;
the multF of R = the multF of R | [: the carrier of R, the carrier of R:]
.= the multF of R || the carrier of R by REALSET1:def 2 ;
then R is Subring of R by A1, A2, C0SP1:def 3;
then Ext_eval (p,(In (x,R))) = In ((eval (p,x)),R) by ALGNUM_1:12;
hence Ext_eval (p,x) = eval (p,x) ; :: thesis: verum