let R be Ring; :: thesis: for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of ()
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 ()
for q being Element of the carrier of ()
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 (); :: thesis: for q being Element of the carrier of ()
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 (); :: 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
.= eval (q,b) by ; :: thesis: verum