let F be Field; :: thesis: for p, q being Polynomial of F
for E being FieldExtension of F
for a being Element of E holds Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))
let p, q be Polynomial of F; :: thesis: for E being FieldExtension of F
for a being Element of E holds Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))
let E be FieldExtension of F; :: thesis: for a being Element of E holds Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))
let a be Element of E; :: thesis: Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a)))
reconsider p1 = p, q1 = q as Polynomial of E by FIELD_4:8;
A: eval ((Subst (p1,q1)),a) = eval (p1,(eval (q1,a))) by POLYNOM5:53;
( q is Element of the carrier of (Polynom-Ring F) & q1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then B: eval (q1,a) = Ext_eval (q,a) by FIELD_4:26;
( p is Element of the carrier of (Polynom-Ring F) & p1 is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
then C: eval ((Subst (p1,q1)),a) = Ext_eval (p,(Ext_eval (q,a))) by B, A, FIELD_4:26;
D: ( Subst (p,q) is Element of the carrier of (Polynom-Ring F) & Subst (p1,q1) is Element of the carrier of (Polynom-Ring E) ) by POLYNOM3:def 10;
Subst (p1,q1) = Subst (p,q) by extsubst;
hence Ext_eval ((Subst (p,q)),a) = Ext_eval (p,(Ext_eval (q,a))) by D, C, FIELD_4:26; :: thesis: verum