let R, S be Ring; :: thesis: ( S is Subring of R implies for p being Polynomial of R
for x being Element of R
for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y) )
assume A1: S is Subring of R ; :: thesis: for p being Polynomial of R
for x being Element of R
for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)
let p be Polynomial of R; :: thesis: for x being Element of R
for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)
let x be Element of R; :: thesis: for q being Polynomial of S
for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)
let q be Polynomial of S; :: thesis: for y being Element of S st p = q & x = y holds
eval (p,x) = eval (q,y)
let y be Element of S; :: thesis: ( p = q & x = y implies eval (p,x) = eval (q,y) )
assume A2: ( p = q & x = y ) ; :: thesis: eval (p,x) = eval (q,y)
A3: ( eval (q,y) in the carrier of S & the carrier of S c= the carrier of R ) by A1, C0SP1:def 3;
thus eval (p,x) = Ext_eval (p,(In (x,R))) by Th39
.= Ext_eval (q,(In (y,R))) by A1, A2, LIOUVIL2:14
.= In ((eval (q,y)),R) by A1, ALGNUM_1:12
.= eval (q,y) by A3, SUBSET_1:def 8 ; :: thesis: verum