let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds FAdj (F,{a}) = FAdj (F,{(- a)})
let E be FieldExtension of F; :: thesis: for a being Element of E holds FAdj (F,{a}) = FAdj (F,{(- a)})
let a be Element of E; :: thesis: FAdj (F,{a}) = FAdj (F,{(- a)})
thus FAdj (F,{a}) = FAdj (F,{(- (- a)),(- a)}) by ext1
.= FAdj (F,{(- a)}) by ext1 ; :: thesis: verum