let F1, F2 be Field; :: thesis: for p being Polynomial of F1
for q being Polynomial of F2
for a being Element of F1
for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)
let p be Polynomial of F1; :: thesis: for q being Polynomial of F2
for a being Element of F1
for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)
let q be Polynomial of F2; :: thesis: for a being Element of F1
for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)
let a be Element of F1; :: thesis: for b being Element of F2 st F1 == F2 & p = q & a = b holds
eval (p,a) = eval (q,b)
let b be Element of F2; :: thesis: ( F1 == F2 & p = q & a = b implies eval (p,a) = eval (q,b) )
assume AS: ( F1 == F2 & p = q & a = b ) ; :: thesis: eval (p,a) = eval (q,b)
then F1 is Subfield of F2 by FIELD_7:def 2;
then A: F2 is FieldExtension of F1 by FIELD_4:7;
( p is Element of the carrier of (Polynom-Ring F1) & q is Element of the carrier of (Polynom-Ring F2) ) by POLYNOM3:def 10;
hence eval (p,a) = eval (q,b) by A, AS, FIELD_4:27; :: thesis: verum