let F1 be Field; :: thesis: for p being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let p be non constant Element of the carrier of (Polynom-Ring F1); :: thesis: for F2 being F1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let F2 be F1 -isomorphic Field; :: thesis: for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2
let h be Isomorphism of F1,F2; :: thesis: ( p splits_in F1 implies (PolyHom h) . p splits_in F2 )
assume AS: p splits_in F1 ; :: thesis: (PolyHom h) . p splits_in F2
defpred S₁[ Nat] means for p being Element of the carrier of (Polynom-Ring F1) st deg p = $1 & p splits_in F1 holds
(PolyHom h) . p splits_in F2;
IA: S₁[1]

proof

now :: thesis: for p being Element of the carrier of (Polynom-Ring F1) st deg p = 1 & p splits_in F1 holds
(PolyHom h) . p splits_in F2

let p be Element of the carrier of (Polynom-Ring F1); :: thesis: ( deg p = 1 & p splits_in F1 implies (PolyHom h) . p splits_in F2 )
assume ( deg p = 1 & p splits_in F1 ) ; :: thesis: (PolyHom h) . p splits_in F2
then deg ((PolyHom h) . p) = 1 by FIELD_1:31;
hence (PolyHom h) . p splits_in F2 by FIELD_4:29; :: thesis: verum

end;

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

end;

IS: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume 1 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for p being Element of the carrier of (Polynom-Ring F1) st deg p = k + 1 & p splits_in F1 holds
(PolyHom h) . p splits_in F2

let p be Element of the carrier of (Polynom-Ring F1); :: thesis: ( deg p = k + 1 & p splits_in F1 implies (PolyHom h) . b₁ splits_in F2 )
assume AS3: ( deg p = k + 1 & p splits_in F1 ) ; :: thesis: (PolyHom h) . b₁ splits_in F2
then consider a being non zero Element of F1, q being Ppoly of F1 such that
A1: p = a * q by FIELD_4:def 5;
reconsider qq = q as Element of the carrier of (Polynom-Ring F1) by POLYNOM3:def 10;
consider G being non empty FinSequence of (Polynom-Ring F1) such that
A2: ( q = Product G & ( for i being Nat st i in dom G holds
ex a being Element of F1 st G . i = rpoly (1,a) ) ) by RING_5:def 4;
deg q = k + 1 by AS3, A1, RING_5:4;
then A3: len G = k + 1 by A2, lemppoly;
consider H being FinSequence, y being object such that
B2: G = H ^ <*y*> by FINSEQ_1:46;
B2a: rng H c= rng G by B2, FINSEQ_1:29;
B2b: rng G c= the carrier of (Polynom-Ring F1) by FINSEQ_1:def 4;
then reconsider H = H as FinSequence of (Polynom-Ring F1) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;
B3: len G = (len H) + (len <*y*>) by B2, FINSEQ_1:22
.= (len H) + 1 by FINSEQ_1:39 ;
rng <*y*> = {y} by FINSEQ_1:39;
then G5: y in rng <*y*> by TARSKI:def 1;
rng <*y*> c= rng G by B2, FINSEQ_1:30;
then reconsider y = y as Element of the carrier of (Polynom-Ring F1) by G5, B2b;
dom <*y*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*y*> by TARSKI:def 1;
then B6: G . (k + 1) = <*y*> . 1 by B2, B3, A3, FINSEQ_1:def 7
.= y ;
dom G = Seg (k + 1) by A3, FINSEQ_1:def 3;
then consider b being Element of F1 such that
B9: y = rpoly (1,b) by A2, B6, FINSEQ_1:4;
deg y = 1 by B9, HURWITZ:27;
then deg ((PolyHom h) . y) = 1 by FIELD_1:31;
then Y: (PolyHom h) . y splits_in F2 by FIELD_4:29;

per cases ( H is empty or not H is empty ) ;

suppose H is empty ; :: thesis: (PolyHom h) . b₁ splits_in F2

then G = <*y*> by B2, FINSEQ_1:34;
then q = rpoly (1,b) by B9, A2, GROUP_4:9;
then deg q = 1 by HURWITZ:27;
then deg p = 1 by A1, RING_5:4;
then deg ((PolyHom h) . p) = 1 by FIELD_1:31;
hence (PolyHom h) . p splits_in F2 by FIELD_4:29; :: thesis: verum

end;

suppose not H is empty ; :: thesis: (PolyHom h) . b₁ splits_in F2

then reconsider H = H as non empty FinSequence of (Polynom-Ring F1) ;
reconsider q1 = Product H as Element of the carrier of (Polynom-Ring F1) ;
C: dom H c= dom G by B2, FINSEQ_1:26;

D: now :: thesis: for i being Nat st i in dom H holds
ex a being Element of F1 st H . i = rpoly (1,a)

let i be Nat; :: thesis: ( i in dom H implies ex a being Element of F1 st H . i = rpoly (1,a) )
assume C0: i in dom H ; :: thesis: ex a being Element of F1 st H . i = rpoly (1,a)
then H . i = G . i by B2, FINSEQ_1:def 7;
hence ex a being Element of F1 st H . i = rpoly (1,a) by C, C0, A2; :: thesis: verum

end;

then reconsider q1p = q1 as Ppoly of F1 by RING_5:def 4;
E: q1p splits_in F1 by lemppolspl;
deg q1 = k by A3, B3, D, lemppoly;
then F: (PolyHom h) . q1 splits_in F2 by E, IV;

now :: thesis: not h . a = 0. F2

assume h . a = 0. F2 ; :: thesis: contradiction
then h . a = h . (0. F1) by RING_2:6;
hence contradiction by FUNCT_2:19; :: thesis: verum

end;

then reconsider ha = h . a as non zero Element of F2 by STRUCT_0:def 12;
reconsider q1h = (PolyHom h) . q1, yh = (PolyHom h) . y as Polynomial of F2 ;
I: q1h *' yh = ((PolyHom h) . q1) * ((PolyHom h) . y) by POLYNOM3:def 10
.= (PolyHom h) . (q1 * y) by FIELD_1:25
.= (PolyHom h) . q by A2, B2, GROUP_4:6 ;
q1h *' yh splits_in F2 by Y, F, lemppolspl1;
then ha * ((PolyHom h) . qq) splits_in F2 by I, lemppolspl2;
hence (PolyHom h) . p splits_in F2 by A1, FIELD_1:26; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(IA, IS);
consider n being Nat such that
H: n = deg p ;
n > 0 by H, RING_4:def 4;
then n >= 1 by NAT_1:14;
hence (PolyHom h) . p splits_in F2 by AS, H, I; :: thesis: verum