let F be Field; :: thesis: for a being Element of F
for p being Polynomial of F
for E being FieldExtension of F
for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q
let a be Element of F; :: thesis: for p being Polynomial of F
for E being FieldExtension of F
for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q
let p be Polynomial of F; :: thesis: for E being FieldExtension of F
for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q
let E be FieldExtension of F; :: thesis: for b being Element of E
for q being Polynomial of E st a = b & p = q holds
a * p = b * q
let b be Element of E; :: thesis: for q being Polynomial of E st a = b & p = q holds
a * p = b * q
let q be Polynomial of E; :: thesis: ( a = b & p = q implies a * p = b * q )
H: F is Subring of E by FIELD_4:def 1;
assume AS: ( a = b & p = q ) ; :: thesis: a * p = b * q

now :: thesis: for o being object st o in NAT holds
(a * p) . o = (b * q) . o

let o be object ; :: thesis: ( o in NAT implies (a * p) . o = (b * q) . o )
assume o in NAT ; :: thesis: (a * p) . o = (b * q) . o
then reconsider i = o as Element of NAT ;
(a * p) . i = a * (p . i) by POLYNOM5:def 4
.= b * (q . i) by AS, H, FIELD_6:16
.= (b * q) . i by POLYNOM5:def 4 ;
hence (a * p) . o = (b * q) . o ; :: thesis: verum

end;

hence a * p = b * q ; :: thesis: verum