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 S1[ 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 S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of the carrier of F st S1[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 S1[x,y]
reconsider y = l . v as Element of F ;
take y ; :: thesis: S1[x,y]
thus S1[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 S1[x,y]
take 0. F ; :: thesis: S1[x, 0. F]
thus S1[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 S1[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 S1[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 S1[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