let F1, F2 be Field; :: thesis: for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let E1 be FieldExtension of F1; :: thesis: for E2 being FieldExtension of F2
for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let E2 be FieldExtension of F2; :: thesis: for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let p be Polynomial of F1; :: thesis: for q being Polynomial of F2
for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let q be Polynomial of F2; :: thesis: for a being Element of E1
for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let a be Element of E1; :: thesis: for b being Element of E2 st F1 == F2 & E1 == E2 & p = q & a = b holds
Ext_eval (p,a) = Ext_eval (q,b)
let b be Element of E2; :: thesis: ( F1 == F2 & E1 == E2 & p = q & a = b implies Ext_eval (p,a) = Ext_eval (q,b) )
assume AS: ( F1 == F2 & E1 == E2 & p = q & a = b ) ; :: thesis: Ext_eval (p,a) = Ext_eval (q,b)
B: ( p is Element of the carrier of (Polynom-Ring F1) & q is Element of the carrier of (Polynom-Ring F2) ) by POLYNOM3:def 10;
p is Polynomial of E1 by FIELD_4:8;
then reconsider p1 = p as Element of the carrier of (Polynom-Ring E1) by POLYNOM3:def 10;
q is Polynomial of E2 by FIELD_4:8;
then reconsider q1 = q as Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;
thus Ext_eval (p,a) = eval (p1,a) by B, FIELD_4:26
.= eval (q1,b) by AS, lift8
.= Ext_eval (q,b) by B, FIELD_4:26 ; :: thesis: verum