let F be Field; :: thesis: for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E
let E be FieldExtension of F; :: thesis: for p being Ppoly of F holds p is Ppoly of E
let p be Ppoly of F; :: thesis: p is Ppoly of E
F is Subfield of E by FIELD_4:7;
then H1: the carrier of F c= the carrier of E by EC_PF_1:def 1;
set PF = Polynom-Ring F;
set PE = Polynom-Ring E;
consider G being non empty FinSequence of (Polynom-Ring F) such that
H2: ( p = Product G & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) ) by RING_5:def 4;
defpred S₁[ Nat] means for G being non empty FinSequence of (Polynom-Ring F) st len G = $1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of E;
IA: S₁[ 0 ] ;

IS: 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 IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for G being non empty FinSequence of (Polynom-Ring F) st len G = k + 1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of E

let G be non empty FinSequence of (Polynom-Ring F); :: thesis: ( len G = k + 1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) implies Product b₁ is Ppoly of E )
assume A: ( len G = k + 1 & ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) ) ; :: thesis: Product b₁ is Ppoly of E

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

suppose S: k = 0 ; :: thesis: Product b₁ is Ppoly of E

then 1 in Seg (len G) by A;
then 1 in dom G by FINSEQ_1:def 3;
then consider a being Element of F such that
A0: G . 1 = rpoly (1,a) by A;
reconsider b = a as Element of E by H1;
H: G = <*(rpoly (1,a))*> by A0, A, S, FINSEQ_1:40;
rpoly (1,a) is Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
then Product G = rpoly (1,a) by H, GROUP_4:9
.= rpoly (1,b) by FIELD_4:21 ;
hence Product G is Ppoly of E by RING_5:51; :: thesis: verum

end;

suppose S: k > 0 ; :: thesis: Product b₁ is Ppoly of E

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 F) by FINSEQ_1:def 4;
then reconsider H = H as FinSequence of (Polynom-Ring F) 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 ;
then reconsider H = H as non empty FinSequence of (Polynom-Ring F) by S, A;
reconsider q = Product H as Polynomial of F by POLYNOM3:def 10;
C: dom H c= dom G by B2, FINSEQ_1:26;

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

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

end;

then reconsider q1 = Product H as Ppoly of E by B3, A, IV;
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 (Polynom-Ring F) 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, A, FINSEQ_1:def 7
.= y ;
dom G = Seg (k + 1) by A, FINSEQ_1:def 3;
then consider a being Element of F such that
B9: y = rpoly (1,a) by A, B6, FINSEQ_1:4;
reconsider b = a as Element of E by H1;
reconsider y1 = rpoly (1,b) as Element of (Polynom-Ring E) by POLYNOM3:def 10;
B8: rpoly (1,b) = rpoly (1,a) by FIELD_4:21;
B7: rpoly (1,b) is Ppoly of E by RING_5:51;
Product G = (Product H) * y by B2, GROUP_4:6
.= q *' (rpoly (1,a)) by B9, POLYNOM3:def 10
.= q1 *' (rpoly (1,b)) by B8, FIELD_4:17 ;
hence Product G is Ppoly of E by B7, RING_5:52; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
J: len G = n ;
thus p is Ppoly of E by I, J, H2; :: thesis: verum