let F be Field; :: thesis: for E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
let E be FieldExtension of F; :: thesis: for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
let a be Element of E; :: thesis: for n being Element of NAT
for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
let n be Element of NAT ; :: thesis: for l being Linear_Combination of VecSp (E,F) ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
let l be Linear_Combination of VecSp (E,F); :: thesis: ex p being Polynomial of F st
( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
set V = VecSp (E,F);
defpred S₁[ object , object ] means ( ex i being Nat st
( i <= n & $1 = i & $2 = l . (a |^ i) ) or ex i being Nat st
( i > n & $1 = i & $2 = 0. F ) );
A: for x being Element of NAT ex y being Element of the carrier of F st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]
reconsider v = a |^ x as Element of (VecSp (E,F)) by FIELD_4:def 6;

per cases ( ex i being Nat st
( i <= n & x = i ) or ex i being Nat st
( i > n & x = i ) ) ;

suppose A1: ex i being Nat st
( i <= n & x = i ) ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

reconsider y = l . v as Element of F ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A1; :: thesis: verum

end;

suppose A1: ex i being Nat st
( i > n & x = i ) ; :: thesis: ex y being Element of the carrier of F st S₁[x,y]

take 0. F ; :: thesis: S₁[x, 0. F]
thus S₁[x, 0. F] by A1; :: thesis: verum

end;

end;

end;

consider p being Function of NAT, the carrier of F such that
B: for x being Element of NAT holds S₁[x,p . x] from FUNCT_2:sch 3(A);
C1: for i being Nat st i <= n holds
p . i = l . (a |^ i)

proof

let i be Nat; :: thesis: ( i <= n implies p . i = l . (a |^ i) )
assume C3: i <= n ; :: thesis: p . i = l . (a |^ i)
i is Element of NAT by ORDINAL1:def 12;
then S₁[i,p . i] by B;
hence l . (a |^ i) = p . i by C3; :: thesis: verum

end;

C2: for i being Nat st i >= n + 1 holds
p . i = 0. F

proof

let i be Nat; :: thesis: ( i >= n + 1 implies p . i = 0. F )
assume C3: i >= n + 1 ; :: thesis: p . i = 0. F
i is Element of NAT by ORDINAL1:def 12;
then S₁[i,p . i] by B;
hence 0. F = p . i by C3, NAT_1:13; :: thesis: verum

end;

then reconsider p = p as Polynomial of F by ALGSEQ_1:def 1;
take p ; :: thesis: ( deg p <= n & ( for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) ) )
n + 1 is_at_least_length_of p by C2, ALGSEQ_1:def 2;
then len p <= n + 1 by ALGSEQ_1:def 3;
then (len p) - 1 <= (n + 1) - 1 by XREAL_1:9;
hence deg p <= n by HURWITZ:def 2; :: thesis: for i being Element of NAT st i <= n holds
p . i = l . (a |^ i)
thus for i being Element of NAT st i <= n holds
p . i = l . (a |^ i) by C1; :: thesis: verum