let R be Ring; 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; 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); 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); 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; for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
let b be Element of S; ( q = p & b = a implies eval (q,b) = eval (p,a) )
assume that
A1:
p = q
and
A2:
a = b
; eval (q,b) = eval (p,a)
thus eval (p,a) =
Ext_eval (p,b)
by A2, Th14
.=
eval (q,b)
by A1, Th15
; verum