let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for x being Element of F holds x = Ext_eval ((x | F),a)
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for x being Element of F holds x = Ext_eval ((x | F),a)
let a be F -algebraic Element of E; :: thesis: for x being Element of F holds x = Ext_eval ((x | F),a)
let x be Element of F; :: thesis: x = Ext_eval ((x | F),a)
thus Ext_eval ((x | F),a) = LC (x | F) by FIELD_6:28
.= x by RING_5:6 ; :: thesis: verum