let F be Field; :: thesis: for E being FieldExtension of F
for T being finite Subset of E st T is F -algebraic holds
FAdj (F,T) = RAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being finite Subset of E st T is F -algebraic holds
FAdj (F,T) = RAdj (F,T)
let T be finite Subset of E; :: thesis: ( T is F -algebraic implies FAdj (F,T) = RAdj (F,T) )
assume AS: T is F -algebraic ; :: thesis: FAdj (F,T) = RAdj (F,T)
defpred S₁[ Nat] means for F being Field
for E being FieldExtension of F
for T being finite Subset of E st card T = $1 & T is F -algebraic holds
FAdj (F,T) = RAdj (F,T);
A: S₁[ 0 ]

proof

now :: thesis: for F being Field
for E being FieldExtension of F
for T being finite Subset of E st card T = 0 holds
FAdj (F,T) = RAdj (F,T)

let F be Field; :: thesis: for E being FieldExtension of F
for T being finite Subset of E st card T = 0 holds
FAdj (F,T) = RAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being finite Subset of E st card T = 0 holds
FAdj (F,T) = RAdj (F,T)
let T be finite Subset of E; :: thesis: ( card T = 0 implies FAdj (F,T) = RAdj (F,T) )
assume card T = 0 ; :: thesis: FAdj (F,T) = RAdj (F,T)
then T = {} ;
then A1: T is Subset of F by XBOOLE_1:2;
then A2: FAdj (F,T) == F by FIELD_7:3;
F == RAdj (F,T) by A1, helpa;
hence FAdj (F,T) = RAdj (F,T) by A2, helpb, FIELD_7:2; :: thesis: verum

end;

hence S₁[ 0 ] ; :: thesis: verum

end;

B: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being Field
for E being FieldExtension of F
for T being finite Subset of E st card T = k + 1 & T is F -algebraic holds
FAdj (F,T) = RAdj (F,T)

let F be Field; :: thesis: for E being FieldExtension of F
for T being finite Subset of E st card T = k + 1 & T is F -algebraic holds
FAdj (F,T) = RAdj (F,T)
let E be FieldExtension of F; :: thesis: for T being finite Subset of E st card T = k + 1 & T is F -algebraic holds
FAdj (F,T) = RAdj (F,T)
let T be finite Subset of E; :: thesis: ( card T = k + 1 & T is F -algebraic implies FAdj (F,T) = RAdj (F,T) )
assume C0: card T = k + 1 ; :: thesis: ( T is F -algebraic implies FAdj (F,T) = RAdj (F,T) )
assume T is F -algebraic ; :: thesis: FAdj (F,T) = RAdj (F,T)
then reconsider T1 = T as non empty finite F -algebraic Subset of E by C0;
set a = the Element of T1;
reconsider a = the Element of T1 as F -algebraic Element of E ;
reconsider T2 = T1 \ {a} as finite F -algebraic Subset of E ;
a in T1 ;
then {a} c= T1 by TARSKI:def 1;
then C4: T1 = T2 \/ {a} by XBOOLE_1:45;
a in {a} by TARSKI:def 1;
then not a in T2 by XBOOLE_0:def 5;
then card T1 = (card T2) + 1 by C4, CARD_2:41;
then C6: FAdj (F,T2) = RAdj (F,T2) by B0, C0;
reconsider E1 = E as FieldExtension of FAdj (F,T2) by FIELD_4:7;
reconsider a1 = a as Element of E1 ;
reconsider E2 = E1 as RingExtension of RAdj (F,T2) by FIELD_4:def 1;
reconsider a2 = a1 as Element of E2 ;
C7: a1 is FAdj (F,T2) -algebraic

proof

consider p being non zero Polynomial of F such that
C8: Ext_eval (p,a) = 0. E by FIELD_6:43;
p <> 0_. F ;
then C9: p <> 0. (Polynom-Ring F) by POLYNOM3:def 10;
reconsider p = p as non zero Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
the carrier of (Polynom-Ring F) c= the carrier of (Polynom-Ring (FAdj (F,T2))) by FIELD_4:10;
then reconsider q = p as Element of the carrier of (Polynom-Ring (FAdj (F,T2))) ;

now :: thesis: not q is zero

assume q is zero ; :: thesis: contradiction
then q = 0_. (FAdj (F,T2)) by UPROOTS:def 5;
then q = 0. (Polynom-Ring (FAdj (F,T2))) by POLYNOM3:def 10;
hence contradiction by C9, FIELD_4:11; :: thesis: verum

end;

then reconsider q = q as non zero Element of the carrier of (Polynom-Ring (FAdj (F,T2))) ;
E1 is FAdj (F,T2) -extending FieldExtension of F ;
then Ext_eval (q,a) = Ext_eval (p,a) by FIELD_7:15;
hence a1 is FAdj (F,T2) -algebraic by C8, FIELD_6:43; :: thesis: verum

end;

FAdj (F,({a} \/ T2)) = FAdj ((FAdj (F,T2)),{a1}) by FIELD_7:34
.= RAdj ((RAdj (F,T2)),{a2}) by C6, C7, FIELD_6:56
.= RAdj (F,({a} \/ T2)) by ug ;
hence FAdj (F,T) = RAdj (F,T) by C4; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider n being Nat such that
H: card T = n ;
thus FAdj (F,T) = RAdj (F,T) by AS, H, I; :: thesis: verum