let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let h be Isomorphism of F1,F2; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E1 be SplittingField of p; :: thesis: for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E2 be SplittingField of (PolyHom h) . p; :: thesis: ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
defpred S₁[ Nat] means for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = $1 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism );

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

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

per cases ( k = 0 or k > 0 ) ;

suppose S: k = 0 ; :: thesis: S₁[b₁]

now :: thesis: for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )

let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let h be Isomorphism of F1,F2; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E1 be SplittingField of p; :: thesis: for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E2 be SplittingField of (PolyHom h) . p; :: thesis: ( card ((Roots (E1,p)) \ the carrier of F1) = 0 implies ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) )
H0: ( p splits_in E1 & (PolyHom h) . p splits_in E2 ) by defspl;
H1: ( F1 is FieldExtension of F1 & F2 is FieldExtension of F2 ) by FIELD_4:6;
H2: ( F1 is Subfield of E1 & F2 is Subfield of E2 ) by FIELD_4:7;
assume card ((Roots (E1,p)) \ the carrier of F1) = 0 ; :: thesis: ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
then (Roots (E1,p)) \ the carrier of F1 = {} ;
then Roots (E1,p) c= the carrier of F1 by XBOOLE_1:37;
then A0: p splits_in F1 by H0, H1, lemma6;
then A1: F1 == E1 by H1, H2, defspl;
then reconsider idF1 = id E1 as Function of E1,F1 ;
(PolyHom h) . p splits_in F2 by A0, lemma6a;
then A2: F2 == E2 by H1, H2, defspl;
then reconsider idF2 = id F2 as Function of F2,E2 ;
reconsider hidF1 = h * idF1 as Function of E1,F2 by FUNCT_2:13;
h * idF1 is Function of E1,F2 by FUNCT_2:13;
then reconsider f = idF2 * (h * idF1) as Function of E1,E2 by FUNCT_2:13;

now :: thesis: for a being Element of E1 holds f . a = h . a

let a be Element of E1; :: thesis: f . a = h . a
a in dom idF1 ;
then K4: (h * idF1) . a = h . (idF1 . a) by FUNCT_1:13
.= h . a ;
reconsider aF = a as Element of F1 by A1;
reconsider ha = h . aF as Element of F2 ;
a in the carrier of F1 by A1;
then ( a in dom idF1 & idF1 . a in dom h ) by FUNCT_2:def 1;
then a in dom (h * idF1) by FUNCT_1:11;
hence f . a = idF2 . (h . a) by K4, FUNCT_1:13
.= ha
.= h . a ;
:: thesis: verum

end;

then K4: f is h -extending by A1;
K5: ( idF1 is isomorphism & idF2 is isomorphism ) by A1, A2, unique20;
then K6: hidF1 is linear ;
hidF1 is onto by A1, FUNCT_2:27;
then f is onto by A2, FUNCT_2:27;
hence ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) by K6, K5, K4; :: thesis: verum

end;

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

end;

suppose S: k > 0 ; :: thesis: S₁[b₁]

now :: thesis: for F1 being Field
for F2 being b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )

let F1 be Field; :: thesis: for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let h be Isomorphism of F1,F2; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E1 be SplittingField of p; :: thesis: for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E2 be SplittingField of (PolyHom h) . p; :: thesis: ( card ((Roots (E1,p)) \ the carrier of F1) = k implies ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) )
assume AS: card ((Roots (E1,p)) \ the carrier of F1) = k ; :: thesis: ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
set a = the Element of (Roots (E1,p)) \ the carrier of F1;
(Roots (E1,p)) \ the carrier of F1 <> {} by AS, S;
then A1: ( the Element of (Roots (E1,p)) \ the carrier of F1 in Roots (E1,p) & not the Element of (Roots (E1,p)) \ the carrier of F1 in the carrier of F1 ) by XBOOLE_0:def 5;
then reconsider a = the Element of (Roots (E1,p)) \ the carrier of F1 as Element of E1 ;
Roots (E1,p) = { b where b is Element of E1 : b is_a_root_of p,E1 } by FIELD_4:def 4;
then consider j being Element of E1 such that
J: ( j = a & j is_a_root_of p,E1 ) by A1;
A2: Ext_eval (p,a) = 0. E1 by J, FIELD_4:def 2;
reconsider a = a as F1 -algebraic Element of E1 ;
set r = MinPoly (a,F1);
consider u being Polynomial of F1 such that
A3: (MinPoly (a,F1)) *' u = p by A2, FIELD_6:53, RING_4:1;
reconsider y = u as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
A4: p = (MinPoly (a,F1)) * y by A3, POLYNOM3:def 10;
reconsider rh = (PolyHom h) . (MinPoly (a,F1)), yh = (PolyHom h) . y as Polynomial of F2 ;
A6: (PolyHom h) . p = ((PolyHom h) . (MinPoly (a,F1))) * ((PolyHom h) . y) by A4, FIELD_1:25
.= rh *' yh by POLYNOM3:def 10 ;
reconsider rhE2 = rh, yhE2 = yh as Polynomial of E2 by FIELD_4:8;
( rhE2 is Element of the carrier of (Polynom-Ring E2) & rh is Element of the carrier of (Polynom-Ring F2) ) by POLYNOM3:def 10;
then deg rhE2 = deg rh by FIELD_4:20;
then A5a: not rhE2 is constant by RING_4:def 4, RATFUNC1:def 2;
yh <> 0_. F2 by A6;
then yhE2 <> 0_. E2 by FIELD_4:12;
then A7a: not yhE2 is zero by UPROOTS:def 5;
A100: rh *' yh = rhE2 *' yhE2 by FIELD_4:17;
rh *' yh splits_in E2 by A6, defspl;
then ex x being non zero Element of E2 ex qx being Ppoly of E2 st rh *' yh = x * qx by FIELD_4:def 5;
then rhE2 splits_in E2 by A5a, A7a, A100, FIELD_4:def 5, lemppolspl3;
then consider rhr being non zero Element of E2, qrh being Ppoly of E2 such that
A9: rh = rhr * qrh by FIELD_4:def 5;
consider b being Element of E2 such that
A11: b is_a_root_of rhr * qrh by POLYNOM5:def 8;
A12: rhr * qrh is Element of the carrier of (Polynom-Ring E2) by POLYNOM3:def 10;
eval ((rhr * qrh),b) = 0. E2 by A11, POLYNOM5:def 7;
then K1: Ext_eval (rh,b) = 0. E2 by A9, A12, FIELD_4:26;
A22: Ext_eval ((MinPoly (a,F1)),a) = 0. E1 by FIELD_6:51;
reconsider b = b as F2 -algebraic Element of E2 ;
K: ( Psi (a,b,h,(MinPoly (a,F1))) is h -extending & Psi (a,b,h,(MinPoly (a,F1))) is isomorphism ) by K1, A22, unique1;
set F1a = FAdj (F1,{a});
reconsider F2b = FAdj (F2,{b}) as FAdj (F1,{a}) -homomorphic FAdj (F1,{a}) -isomorphic Field by K, RING_2:def 4, RING_3:def 4;
reconsider g = Psi (a,b,h,(MinPoly (a,F1))) as Isomorphism of (FAdj (F1,{a})),F2b by K;
reconsider E1a = E1 as FieldExtension of FAdj (F1,{a}) by FIELD_4:7;
reconsider E2a = E2 as FieldExtension of F2b by FIELD_4:7;
the carrier of (Polynom-Ring F1) c= the carrier of (Polynom-Ring (FAdj (F1,{a}))) by FIELD_4:10;
then reconsider f = p as Element of the carrier of (Polynom-Ring (FAdj (F1,{a}))) ;
( deg f = deg p & deg p > 0 ) by FIELD_4:20, RING_4:def 4;
then reconsider f = f as non constant Element of the carrier of (Polynom-Ring (FAdj (F1,{a}))) by RING_4:def 4;
reconsider E1a = E1a as SplittingField of f by splift;
reconsider aa = a as Element of E1a ;
(PolyHom g) . f = (PolyHom h) . p

proof

now :: thesis: for i being Nat holds ((PolyHom g) . f) . i = ((PolyHom h) . p) . i

let i be Nat; :: thesis: ((PolyHom g) . f) . i = ((PolyHom h) . p) . i
thus ((PolyHom g) . f) . i = g . (f . i) by FIELD_1:def 2
.= h . (p . i) by K
.= ((PolyHom h) . p) . i by FIELD_1:def 2 ; :: thesis: verum

end;

hence (PolyHom g) . f = (PolyHom h) . p ; :: thesis: verum

end;

then reconsider E2a = E2a as SplittingField of (PolyHom g) . f by splift;
K8: {a} is Subset of (FAdj (F1,{a})) by FIELD_6:35;
K7: a in {a} by TARSKI:def 1;
Ext_eval (f,aa) = 0. E1a by A2, lemma7b;
then aa is_a_root_of f,E1a by FIELD_4:def 2;
then a in { x where x is Element of E1a : x is_a_root_of f,E1a } ;
then K6: a in Roots (E1a,f) by FIELD_4:def 4;
K4: a in (Roots (E1a,f)) \ the carrier of F1 by A1, K6, XBOOLE_0:def 5;
K5: not a in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) by K7, K8, XBOOLE_0:def 5;
(Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) c= (Roots (E1a,f)) \ the carrier of F1

proof

now :: thesis: for o being object st o in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) holds
o in (Roots (E1a,f)) \ the carrier of F1

let o be object ; :: thesis: ( o in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) implies o in (Roots (E1a,f)) \ the carrier of F1 )
assume L: o in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) ; :: thesis: o in (Roots (E1a,f)) \ the carrier of F1
F1 is Subfield of FAdj (F1,{a}) by FIELD_4:7;
then the carrier of F1 c= the carrier of (FAdj (F1,{a})) by EC_PF_1:def 1;
then ( o in Roots (E1a,f) & not o in the carrier of F1 ) by L, XBOOLE_0:def 5;
hence o in (Roots (E1a,f)) \ the carrier of F1 by XBOOLE_0:def 5; :: thesis: verum

end;

hence (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) c= (Roots (E1a,f)) \ the carrier of F1 ; :: thesis: verum

end;

then (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) c< (Roots (E1a,f)) \ the carrier of F1 by K4, K5, XBOOLE_0:def 8;
then L2: card ((Roots (E1a,f)) \ the carrier of (FAdj (F1,{a}))) < card ((Roots (E1a,f)) \ the carrier of F1) by CARD_2:48;
card ((Roots (E1a,f)) \ the carrier of F1) = k by AS, m4spl;
then consider h1 being Function of E1a,E2a such that
L1: ( h1 is g -extending & h1 is isomorphism ) by IV, L2;
reconsider h1 = h1 as Function of E1,E2 ;
thus ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) by L1, K, e1a; :: thesis: verum

end;

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

end;

end;

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 4(II);
consider n being Nat such that
H: card ((Roots (E1,p)) \ the carrier of F1) = n ;
thus ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) by H, I; :: thesis: verum