let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )
let a be F -algebraic Element of E; :: thesis: ( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )
H: F is Subring of E by FIELD_4:def 1;
thus 0. (FAdj (F,{a})) = 0. E by FIELD_6:def 6
.= Ext_eval ((0_. F),a) by ALGNUM_1:13 ; :: thesis: 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a)
thus 1. (FAdj (F,{a})) = 1. E by FIELD_6:def 6
.= Ext_eval ((1_. F),a) by H, ALGNUM_1:14 ; :: thesis: verum