let F be Field; :: thesis: for E being FieldExtension of F
for p being Polynomial of F
for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q
let E be FieldExtension of F; :: thesis: for p being Polynomial of F
for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q
let p be Polynomial of F; :: thesis: for q being Polynomial of E
for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q
let q be Polynomial of E; :: thesis: for a being Element of F
for b being Element of E st p = q & a = b holds
a * p = b * q
let a be Element of F; :: thesis: for b being Element of E st p = q & a = b holds
a * p = b * q
let b be Element of E; :: thesis: ( p = q & a = b implies a * p = b * q )
assume AS: ( p = q & a = b ) ; :: thesis: a * p = b * q
then A: a | F = b | E by FIELD_6:23;
thus a * p = (a | F) *' p by FIELD_8:2
.= (b | E) *' q by A, AS, FIELD_4:17
.= b * q by FIELD_8:2 ; :: thesis: verum