let F be Field; :: thesis: for E being F -finite FieldExtension of F st ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p holds
for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E
let E be F -finite FieldExtension of F; :: thesis: ( ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p implies for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E )
assume ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p ; :: thesis: for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E
then consider p being non constant Element of the carrier of (Polynom-Ring F) such that
AS: E is SplittingField of p ;
reconsider U = E as SplittingField of p by AS;
B: doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) = doubleLoopStr(# the carrier of (FAdj (F,(Roots (E,p)))), the addF of (FAdj (F,(Roots (E,p)))), the multF of (FAdj (F,(Roots (E,p)))), the OneF of (FAdj (F,(Roots (E,p)))), the ZeroF of (FAdj (F,(Roots (E,p)))) #) by AS, FIELD_8:34, FIELD_7:def 1;

now :: thesis: for K1 being FieldExtension of E
for h being F -fixing Monomorphism of E,K1 holds h is Automorphism of E

let K1 be FieldExtension of E; :: thesis: for h being F -fixing Monomorphism of E,K1 holds h is Automorphism of E
let h be F -fixing Monomorphism of E,K1; :: thesis: h is Automorphism of E
reconsider K = K1 as E -extending FieldExtension of F ;
p splits_in E by AS, FIELD_8:def 1;
then h .: (Roots (U,p)) c= the carrier of E by lemNor2b;
then C: h .: the carrier of (FAdj (F,(Roots (E,p)))) c= the carrier of E by lemNor2c;
reconsider g = h | the carrier of E as Function of E,E by B, C, FUNCT_2:101;
D: E is Subfield of K by FIELD_4:7;
( g is additive & g is multiplicative & g is unity-preserving )

proof

now :: thesis: for x, y being Element of E holds g . (x + y) = (g . x) + (g . y)

let x, y be Element of E; :: thesis: g . (x + y) = (g . x) + (g . y)
dom h = the carrier of E by FUNCT_2:def 1;
then ( h . x in h .: the carrier of E & h . y in h .: the carrier of E ) by FUNCT_1:def 6;
then reconsider a = h . x, b = h . y as Element of E by B, C;
E: [a,b] in [: the carrier of E, the carrier of E:] ;
thus g . (x + y) = (h . x) + (h . y) by VECTSP_1:def 20
.= ( the addF of K || the carrier of E) . (a,b) by E, FUNCT_1:49
.= (g . x) + (g . y) by D, EC_PF_1:def 1 ; :: thesis: verum

end;

hence g is additive ; :: thesis: ( g is multiplicative & g is unity-preserving )

now :: thesis: for x, y being Element of E holds g . (x * y) = (g . x) * (g . y)

let x, y be Element of E; :: thesis: g . (x * y) = (g . x) * (g . y)
dom h = the carrier of E by FUNCT_2:def 1;
then ( h . x in h .: the carrier of E & h . y in h .: the carrier of E ) by FUNCT_1:def 6;
then reconsider a = h . x, b = h . y as Element of E by B, C;
E: [a,b] in [: the carrier of E, the carrier of E:] ;
thus g . (x * y) = (h . x) * (h . y) by GROUP_6:def 6
.= ( the multF of K || the carrier of E) . (a,b) by E, FUNCT_1:49
.= (g . x) * (g . y) by D, EC_PF_1:def 1 ; :: thesis: verum

end;

hence g is multiplicative ; :: thesis: g is unity-preserving
g . (1_ E) = 1_ K by GROUP_1:def 13
.= 1. E by D, EC_PF_1:def 1 ;
hence g is unity-preserving ; :: thesis: verum

end;

then reconsider g = g as Monomorphism of E ;
for a being Element of F holds g . a = a by FIELD_8:def 2;
then g is F -fixing by FIELD_8:def 2;
hence h is Automorphism of E ; :: thesis: verum

end;

hence for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E ; :: thesis: verum