let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S)
for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let S be RingExtension of R; :: thesis: for p being Element of the carrier of (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S)
for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let p be Element of the carrier of (Polynom-Ring R); :: thesis: for q being Element of the carrier of (Polynom-Ring S)
for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let q be Element of the carrier of (Polynom-Ring S); :: thesis: for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let a be Element of R; :: thesis: for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let b be Element of S; :: thesis: ( q = p & b = a implies eval (q,b) = eval (p,a) )
assume that
A1: p = q and
A2: a = b ; :: thesis: eval (q,b) = eval (p,a)
thus eval (p,a) = Ext_eval (p,b) by A2, Th14
.= eval (q,b) by A1, Th15 ; :: thesis: verum