let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E holds
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
let E be FieldExtension of F; :: thesis: for a being Element of E holds
( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
let a be Element of E; :: thesis: ( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic )
reconsider E1 = E as Polynom-Ring F -homomorphic Field ;
reconsider g = hom_Ext_eval (a,F) as Homomorphism of (Polynom-Ring F),E1 ;
H: (Polynom-Ring F) / (ker g), Image g are_isomorphic by RING_2:15;

A: now :: thesis: ( a is F -transcendental implies Polynom-Ring F, RAdj (F,{a}) are_isomorphic )

assume a is F -transcendental ; :: thesis: Polynom-Ring F, RAdj (F,{a}) are_isomorphic
then (Polynom-Ring F) / (ker g), Polynom-Ring F are_isomorphic by RING_2:17;
then Polynom-Ring F, Image g are_isomorphic by H, RING_3:44;
hence Polynom-Ring F, RAdj (F,{a}) are_isomorphic by lemphi4; :: thesis: verum

end;

now :: thesis: ( RAdj (F,{a}), Polynom-Ring F are_isomorphic implies a is F -transcendental )

assume RAdj (F,{a}), Polynom-Ring F are_isomorphic ; :: thesis: a is F -transcendental
then Polynom-Ring F is RAdj (F,{a}) -isomorphic by RING_3:def 4;
then RAdj (F,{a}) <> FAdj (F,{a}) ;
hence a is F -transcendental by ch1; :: thesis: verum

end;

hence ( a is F -transcendental iff RAdj (F,{a}), Polynom-Ring F are_isomorphic ) by A; :: thesis: verum