let R be non degenerated comRing; :: thesis: for S being comRingExtension of R
for n being Ordinal
for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let S be comRingExtension of R; :: thesis: for n being Ordinal
for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let n be Ordinal; :: thesis: for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let P be non empty Subset of (Polynom-Ring (n,R)); :: thesis: for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let F be LeftLinearCombination of P; :: thesis: for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let p be Polynomial of n,R; :: thesis: ( p = Sum F implies for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) )
assume AS: p = Sum F ; :: thesis: for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let x be Function of n,S; :: thesis: ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
defpred S₁[ Nat] means for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P st len F = $1 holds
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) );
H: R is Subring of S by FIELD_4:def 1;
IA: S₁[ 0 ]

proof

now :: thesis: for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P st len F = 0 holds
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )

let P be non empty Subset of (Polynom-Ring (n,R)); :: thesis: for F being LeftLinearCombination of P st len F = 0 holds
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let F be LeftLinearCombination of P; :: thesis: ( len F = 0 implies for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) )
assume A1: len F = 0 ; :: thesis: for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let p be Polynomial of n,R; :: thesis: ( p = Sum F implies for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) )
assume A2: p = Sum F ; :: thesis: for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let x be Function of n,S; :: thesis: ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
thus ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) :: thesis: verum

proof

take G = <*> the carrier of S; :: thesis: ( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
thus len G = len F by A1; :: thesis: ( Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
F = <*> the carrier of (Polynom-Ring (n,R)) by A1;
then Sum F = 0. (Polynom-Ring (n,R)) by RLVECT_1:43;
then p = 0_ (n,R) by A2, POLYNOM1:def 11;
hence Ext_eval (p,x) = 0. S by ev0
.= Sum G by RLVECT_1:43 ;
:: thesis: for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x)
thus for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ; :: thesis: verum

end;

end;

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

end;

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 P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P st len F = k + 1 holds
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )

let P be non empty Subset of (Polynom-Ring (n,R)); :: thesis: for F being LeftLinearCombination of P st len F = k + 1 holds
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let F be LeftLinearCombination of P; :: thesis: ( len F = k + 1 implies for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) )
assume I1: len F = k + 1 ; :: thesis: for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let p be Polynomial of n,R; :: thesis: ( p = Sum F implies for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) )
assume I2: p = Sum F ; :: thesis: for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
let x be Function of n,S; :: thesis: ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )
set PR = Polynom-Ring (n,R);
set PS = Polynom-Ring (n,S);
F <> {} by I1;
then consider K being LeftLinearCombination of P, a being Element of (Polynom-Ring (n,R)) such that
I3: ( F = K ^ <*a*> & <*a*> is LeftLinearCombination of P ) by IDEAL_1:33;
I4: len F = (len K) + (len <*a*>) by I3, FINSEQ_1:22
.= (len K) + 1 by FINSEQ_1:39 ;
reconsider r = Sum K as Polynomial of n,R by POLYNOM1:def 11;
consider GK being FinSequence of S such that
I5: ( len GK = len K & Ext_eval (r,x) = Sum GK & ( for i being set st i in dom GK holds
for q being Polynomial of n,R st q = K . i holds
GK . i = Ext_eval (q,x) ) ) by IV, I1, I4;
I9: Sum <*a*> = a by RLVECT_1:44;
reconsider pa = a as Polynomial of n,R by POLYNOM1:def 11;
set G = GK ^ <*(Ext_eval (pa,x))*>;
len <*(Ext_eval (pa,x))*> = 1 by FINSEQ_1:39;
then I6: len (GK ^ <*(Ext_eval (pa,x))*>) = len F by I4, I5, FINSEQ_1:22;
p = (Sum K) + (Sum <*a*>) by I2, I3, RLVECT_1:41;
then I8: r + pa = p by I9, POLYNOM1:def 11;
I7: Sum (GK ^ <*(Ext_eval (pa,x))*>) = (Sum GK) + (Sum <*(Ext_eval (pa,x))*>) by RLVECT_1:41
.= (Ext_eval (r,x)) + (Ext_eval (pa,x)) by I5, RLVECT_1:44
.= Ext_eval (p,x) by I8, H, evalpl ;

now :: thesis: for i being set st i in dom (GK ^ <*(Ext_eval (pa,x))*>) holds
for q being Polynomial of n,R st q = F . i holds
(GK ^ <*(Ext_eval (pa,x))*>) . i = Ext_eval (q,x)

let i be set ; :: thesis: ( i in dom (GK ^ <*(Ext_eval (pa,x))*>) implies for q being Polynomial of n,R st q = F . i holds
(GK ^ <*(Ext_eval (pa,x))*>) . b₂ = Ext_eval (b₃,x) )
assume J1: i in dom (GK ^ <*(Ext_eval (pa,x))*>) ; :: thesis: for q being Polynomial of n,R st q = F . i holds
(GK ^ <*(Ext_eval (pa,x))*>) . b₂ = Ext_eval (b₃,x)
let q be Polynomial of n,R; :: thesis: ( q = F . i implies (GK ^ <*(Ext_eval (pa,x))*>) . b₁ = Ext_eval (b₂,x) )
assume J2: q = F . i ; :: thesis: (GK ^ <*(Ext_eval (pa,x))*>) . b₁ = Ext_eval (b₂,x)

per cases ( i in dom GK or ex k being Nat st
( k in dom <*(Ext_eval (pa,x))*> & i = (len GK) + k ) ) by J1, FINSEQ_1:25;

suppose J3: i in dom GK ; :: thesis: (GK ^ <*(Ext_eval (pa,x))*>) . b₁ = Ext_eval (b₂,x)

then J4: GK . i = (GK ^ <*(Ext_eval (pa,x))*>) . i by FINSEQ_1:def 7;
dom K = Seg (len GK) by I5, FINSEQ_1:def 3
.= dom GK by FINSEQ_1:def 3 ;
then K . i = F . i by J3, I3, FINSEQ_1:def 7;
hence (GK ^ <*(Ext_eval (pa,x))*>) . i = Ext_eval (q,x) by J2, J3, J4, I5; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom <*(Ext_eval (pa,x))*> & i = (len GK) + k ) ; :: thesis: (GK ^ <*(Ext_eval (pa,x))*>) . b₁ = Ext_eval (b₂,x)

then consider k being Nat such that
J3: ( k in dom <*(Ext_eval (pa,x))*> & i = (len GK) + k ) ;
J6: dom <*(Ext_eval (pa,x))*> = {1} by FINSEQ_1:38, FINSEQ_1:2;
then J4: k = 1 by J3, TARSKI:def 1;
k in dom <*a*> by J6, J3, FINSEQ_1:2, FINSEQ_1:38;
then J5: F . i = <*a*> . 1 by J4, J3, I5, I3, FINSEQ_1:def 7
.= a ;
thus (GK ^ <*(Ext_eval (pa,x))*>) . i = <*(Ext_eval (pa,x))*> . 1 by J4, J3, FINSEQ_1:def 7
.= Ext_eval (q,x) by J5, J2 ; :: thesis: verum

end;

end;

end;

hence ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) by I6, I7; :: thesis: verum

end;

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

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
thus ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) ) by AS, I; :: thesis: verum