let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
Roots (K,p) = Roots (E,p)
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
Roots (K,p) = Roots (E,p)
let K be F -extending FieldExtension of F; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F) st p splits_in E holds
Roots (K,p) = Roots (E,p)
let p be non constant Element of the carrier of (Polynom-Ring F); :: thesis: ( p splits_in E implies Roots (K,p) = Roots (E,p) )
assume AS: p splits_in E ; :: thesis: Roots (K,p) = Roots (E,p)
then p splits_in K by FIELD_8:19;
hence Roots (K,p) = Roots (E,p) by AS, FIELD_8:29; :: thesis: verum