let F be Field; :: thesis: for E being FieldExtension of F
for a being F -algebraic Element of E
for f, g being F -fixing Automorphism of (FAdj (F,{a})) st f . a = g . a holds
f = g
let E be FieldExtension of F; :: thesis: for a being F -algebraic Element of E
for f, g being F -fixing Automorphism of (FAdj (F,{a})) st f . a = g . a holds
f = g
let a be F -algebraic Element of E; :: thesis: for f, g being F -fixing Automorphism of (FAdj (F,{a})) st f . a = g . a holds
f = g
let f, g be F -fixing Automorphism of (FAdj (F,{a})); :: thesis: ( f . a = g . a implies f = g )
assume AS: f . a = g . a ; :: thesis: f = g
A: E is Polynom-Ring F -homomorphic FieldExtension of F ;
then B: the carrier of (FAdj (F,{a})) = the carrier of (RAdj (F,{a})) by FIELD_6:56
.= { (Ext_eval (p,a)) where p is Polynomial of F : verum } by A, FIELD_6:45 ;
defpred S₁[ Nat] means for p being Polynomial of F st deg p = $1 holds
f . (Ext_eval (p,a)) = g . (Ext_eval (p,a));

IA: now :: thesis: for p being non zero Polynomial of F holds f . (Ext_eval ((LM p),a)) = g . (Ext_eval ((LM p),a))

let p be non zero Polynomial of F; :: thesis: f . (Ext_eval ((LM p),a)) = g . (Ext_eval ((LM p),a))
F is Subfield of FAdj (F,{a}) by FIELD_4:7;
then the carrier of F c= the carrier of (FAdj (F,{a})) by EC_PF_1:def 1;
then reconsider b = LC p as Element of (FAdj (F,{a})) ;
( a in {a} & {a} is Subset of (FAdj (F,{a})) ) by TARSKI:def 1, FIELD_6:35;
then reconsider a1 = a as Element of (FAdj (F,{a})) ;
A: Ext_eval ((LM p),a1) = b * (a1 |^ (deg p)) by FIELD_6:29;
( E is FAdj (F,{a}) -extending & LM p is Element of the carrier of (Polynom-Ring F) ) by FIELD_4:7, POLYNOM3:def 10;
then B: Ext_eval ((LM p),a) = Ext_eval ((LM p),a1) by FIELD_6:11;
( id (FAdj (F,{a})) is additive & id (FAdj (F,{a})) is multiplicative & id (FAdj (F,{a})) is unity-preserving ) ;
then C: FAdj (F,{a}) is FAdj (F,{a}) -homomorphic by RING_2:def 4;
thus f . (Ext_eval ((LM p),a)) = (f . b) * (f . (a1 |^ (deg p))) by A, B, GROUP_6:def 6
.= b * (f . (a1 |^ (deg p))) by FIELD_8:def 2
.= b * ((f . a1) |^ (deg p)) by C, lemID
.= b * (g . (a1 |^ (deg p))) by AS, C, lemID
.= (g . b) * (g . (a1 |^ (deg p))) by FIELD_8:def 2
.= g . (Ext_eval ((LM p),a)) by A, B, GROUP_6:def 6 ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume IV: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]

now :: thesis: for p being Polynomial of F st deg p = k holds
f . (Ext_eval (p,a)) = g . (Ext_eval (p,a))

let p be Polynomial of F; :: thesis: ( deg p = k implies f . (Ext_eval (b₁,a)) = g . (Ext_eval (b₁,a)) )
assume A0: deg p = k ; :: thesis: f . (Ext_eval (b₁,a)) = g . (Ext_eval (b₁,a))
then H1: p <> 0_. F by HURWITZ:20;
then consider q being Polynomial of F such that
A1: ( len q < len p & p = q + (LM p) & ( for n being Element of NAT st n < (len p) - 1 holds
q . n = p . n ) ) by POLYNOM4:16, POLYNOM4:5;
H2: not p is zero by H1, UPROOTS:def 5;

per cases ( q = 0_. F or q <> 0_. F ) ;

suppose q = 0_. F ; :: thesis: f . (Ext_eval (b₁,a)) = g . (Ext_eval (b₁,a))

hence f . (Ext_eval (p,a)) = g . (Ext_eval (p,a)) by A1, H2, IA; :: thesis: verum

end;

suppose q <> 0_. F ; :: thesis: f . (Ext_eval (b₁,a)) = g . (Ext_eval (b₁,a))

then reconsider degq = deg q as Nat by FIELD_1:1;
deg p = (len p) - 1 by HURWITZ:def 2;
then H: len q < k + 1 by A0, A1;
deg q = (len q) - 1 by HURWITZ:def 2;
then len q = (deg q) + 1 ;
then degq < k by XREAL_1:6, H;
then A3: f . (Ext_eval (q,a)) = g . (Ext_eval (q,a)) by IV;
A4: f . (Ext_eval ((LM p),a)) = g . (Ext_eval ((LM p),a)) by H2, IA;
A5: F is Subring of E by FIELD_4:def 1;
( Ext_eval (q,a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } & Ext_eval ((LM p),a) in { (Ext_eval (p,a)) where p is Polynomial of F : verum } ) ;
then reconsider u = Ext_eval (q,a), v = Ext_eval ((LM p),a) as Element of the carrier of (FAdj (F,{a})) by B;
A7: Ext_eval ((q + (LM p)),a) = (Ext_eval (q,a)) + (Ext_eval ((LM p),a)) by A5, ALGNUM_1:15;
A8: FAdj (F,{a}) is Subring of E by FIELD_5:12;
thus f . (Ext_eval (p,a)) = f . (u + v) by A1, A7, A8, FIELD_6:15
.= (f . u) + (f . v) by VECTSP_1:def 20
.= g . (u + v) by A3, A4, VECTSP_1:def 20
.= g . (Ext_eval (p,a)) by A1, A7, A8, FIELD_6:15 ; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(IS);

now :: thesis: for o being object st o in the carrier of (FAdj (F,{a})) holds
f . o = g . o

let o be object ; :: thesis: ( o in the carrier of (FAdj (F,{a})) implies f . b₁ = g . b₁ )
assume o in the carrier of (FAdj (F,{a})) ; :: thesis: f . b₁ = g . b₁
then consider p being Polynomial of F such that
C: o = Ext_eval (p,a) by B;

per cases ( p = 0_. F or p <> 0_. F ) ;

suppose p = 0_. F ; :: thesis: f . b₁ = g . b₁

then Ext_eval (p,a) = 0. E by ALGNUM_1:13
.= 0. (FAdj (F,{a})) by FIELD_6:def 6 ;
hence f . o = g . o by C; :: thesis: verum

end;

suppose p <> 0_. F ; :: thesis: f . b₁ = g . b₁

then deg p is natural by FIELD_1:1;
then deg p in NAT by ORDINAL1:def 12;
hence f . o = g . o by C, I; :: thesis: verum

end;

end;

end;

hence f = g ; :: thesis: verum