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

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