let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let p, q be Polynomial of F; :: thesis:
let p1, q1 be Polynomial of E; :: thesis:
assume AS: ( p1 = p & q1 = q ) ; :: thesis:
consider f being FinSequence of the carrier of (Polynom-Ring F) such that
A1: ( Subst (p,q) = Sum f & len f = len p & ( for n being Element of NAT st n in dom f holds
f . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) by POLYNOM5:def 6;
consider g being FinSequence of the carrier of (Polynom-Ring E) such that
A2: ( Subst (p1,q1) = Sum g & len g = len p1 & ( for n being Element of NAT st n in dom g holds
g . n = (p1 . (n -' 1)) * (q1 `^ (n -' 1)) ) ) by POLYNOM5:def 6;
( 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 deg p1 = deg p by AS, FIELD_4:20;
then deg p = (len p1) - 1 by HURWITZ:def 2;
then H1: (len p) - 1 = (len p1) - 1 by HURWITZ:def 2;
A3: f = g

B1: dom f = Seg (len p1) by H1, A1, FINSEQ_1:def 3
.= dom g by A2, FINSEQ_1:def 3 ;

let n be Element of NAT ; :: thesis:
assume B2: n in dom f ; :: thesis:
n -' 1 is Element of NAT by ORDINAL1:def 12;
then B3: ( q `^ (n -' 1) = q1 `^ (n -' 1) & p . (n -' 1) = p1 . (n -' 1) ) by AS, multi00;
B4: (p . (n -' 1)) | F = (p1 . (n -' 1)) | E by AS, FIELD_6:23;
thus f . n = (p . (n -' 1)) * (q `^ (n -' 1)) by B2, A1
.= ((p . (n -' 1)) | F) *' (q `^ (n -' 1)) by FIELD_8:2
.= ((p1 . (n -' 1)) | E) *' (q1 `^ (n -' 1)) by B3, B4, FIELD_4:17
.= (p1 . (n -' 1)) * (q1 `^ (n -' 1)) by FIELD_8:2
.= g . n by A2, B1, B2 ; :: thesis:

end;

hence f = g by B1; :: thesis:

end;