let F be Field; :: thesis:
let E be FieldExtension of F; :: thesis:
let T be non empty finite Subset of E; :: thesis:
let p be Polynomial of (card T),F; :: thesis:
let x be T -evaluating Function of (card T),E; :: thesis:
set n = card T;
set R = F;
A0: F is Subring of E by FIELD_4:def 1;
defpred S₁[ Nat] means for p being Polynomial of (card T),F st card (Support p) = $1 holds
Ext_eval (p,x) in the carrier of (RAdj (F,T));
A1: ex k being Element of NAT st card (Support p) = k ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

proof

let u be object ; :: thesis:
assume A10: u in Support r1 ; :: thesis:
then reconsider u = u as Element of Bags (card T) ;

now :: thesis:

assume A11: u = bg ; :: thesis:
then u in dom (bg .--> (0. F)) by TARSKI:def 1;
then r1 . u = (bg .--> (0. F)) . bg by A9, A11, FUNCT_4:13;
then r1 . u = 0. F by FUNCOP_1:72;
hence contradiction by A10, POLYNOM1:def 4; :: thesis:

end;

then not u in dom (bg .--> (0. F)) by TARSKI:def 1;
then p . u = r1 . u by A9, FUNCT_4:11;
then p . u <> 0. F by A10, POLYNOM1:def 4;
hence u in Support p by POLYNOM1:def 4; :: thesis:

end;

then Support r1 c= Support p ;
then reconsider r1 = r1 as Polynomial of (card T),F by POLYNOM1:def 5;
A12: dom p = Bags (card T) by FUNCT_2:def 1;
A13: for u being object st u in Support p holds
u in (Support r1) \/ {bg}

proof

let u be object ; :: thesis:
assume A14: u in Support p ; :: thesis:
then reconsider u = u as Element of Bags (card T) ;
A15: p . u <> 0. F by A14, POLYNOM1:def 4;

per cases ;

suppose u = bg ; :: thesis:

then u in {bg} by TARSKI:def 1;
hence u in (Support r1) \/ {bg} by XBOOLE_0:def 3; :: thesis:

end;

suppose u <> bg ; :: thesis:

then not u in dom (bg .--> (0. F)) by TARSKI:def 1;
then r1 . u = p . u by A9, FUNCT_4:11;
then u in Support r1 by A15, POLYNOM1:def 4;
hence u in (Support r1) \/ {bg} by XBOOLE_0:def 3; :: thesis:

end;

bg in dom (bg .--> (0. F)) by TARSKI:def 1;
then r1 . bg = (bg .--> (0. F)) . bg by A9, FUNCT_4:13;
then A16: r1 . bg = 0. F by FUNCOP_1:72;
then A17: not bg in Support r1 by POLYNOM1:def 4;
for u being object st u in (Support r1) \/ {bg} holds
u in Support p

proof

let u be object ; :: thesis:
assume A18: u in (Support r1) \/ {bg} ; :: thesis:

per cases by A18, XBOOLE_0:def 3;

suppose A19: u in Support r1 ; :: thesis:

then reconsider u = u as Element of Bags (card T) ;
u <> bg by A16, A19, POLYNOM1:def 4;
then not u in dom (bg .--> (0. F)) by TARSKI:def 1;
then A20: r1 . u = p . u by A9, FUNCT_4:11;
r1 . u <> 0. F by A19, POLYNOM1:def 4;
hence u in Support p by A20, POLYNOM1:def 4; :: thesis:

end;

suppose u in {bg} ; :: thesis:

hence u in Support p by A7, TARSKI:def 1; :: thesis:

end;

proof

let u be object ; :: thesis:
assume A24: u in Support r2 ; :: thesis:
then reconsider u = u as Element of Bags (card T) ;
A25: r2 . u <> 0. F by A24, POLYNOM1:def 4;

now :: thesis:

assume u <> bg ; :: thesis:
then not u in dom (bg .--> (p . bg)) by TARSKI:def 1;
then r2 . u = (0_ ((card T),F)) . u by A22, FUNCT_4:11;
hence contradiction by A25, POLYNOM1:22; :: thesis:

end;

hence u in {bg} by TARSKI:def 1; :: thesis:

end;

A50: for u being object st u in {bg} holds
u in Support r2

proof

let u be object ; :: thesis:
bg in dom (bg .--> (p . bg)) by TARSKI:def 1;
then r2 . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A26: r2 . bg = p . bg by FUNCOP_1:72;
assume u in {bg} ; :: thesis:
then u = bg by TARSKI:def 1;
hence u in Support r2 by A8, A26, POLYNOM1:def 4; :: thesis:

end;

then Support r2 = {bg} by A23, TARSKI:2;
then reconsider r2 = r2 as Polynomial of (card T),F by POLYNOM1:def 5;
A28: for u being object st u in Bags (card T) holds
(r1 + r2) . u = p . u

proof

let u be object ; :: thesis:
assume u in Bags (card T) ; :: thesis:
then reconsider u = u as bag of card T ;

per cases ;

suppose A29: u = bg ; :: thesis:

bg in dom (bg .--> (p . bg)) by TARSKI:def 1;
then r2 . bg = (bg .--> (p . bg)) . bg by A22, FUNCT_4:13;
then A30: r2 . bg = p . bg by FUNCOP_1:72;
u in dom (bg .--> (0. F)) by A29, TARSKI:def 1;
then A31: r1 . u = (bg .--> (0. F)) . bg by A9, A29, FUNCT_4:13;
(r1 + r2) . u = (r1 . u) + (r2 . u) by POLYNOM1:15
.= (0. F) + (p . bg) by A29, A31, A30, FUNCOP_1:72
.= p . bg ;
hence (r1 + r2) . u = p . u by A29; :: thesis:

end;

suppose A32: u <> bg ; :: thesis:

then A33: not u in dom (bg .--> (0. F)) by TARSKI:def 1;
not u in dom (bg .--> (p . bg)) by A32, TARSKI:def 1;
then r2 . u = (0_ ((card T),F)) . u by A22, FUNCT_4:11;
then A34: r2 . u = 0. F by POLYNOM1:22;
(r1 + r2) . u = (r1 . u) + (r2 . u) by POLYNOM1:15
.= p . u by A9, A33, A34, FUNCT_4:11 ;
hence (r1 + r2) . u = p . u ; :: thesis:

end;

reconsider a = Ext_eval (r1,x) as Element of (RAdj (F,T)) by A3, A21;
reconsider c = Ext_eval (r2,x) as Element of (RAdj (F,T)) by A50, A23, TARSKI:2, Lm7;
dom (r1 + r2) = Bags (card T) by FUNCT_2:def 1;
then Ext_eval (p,x) = Ext_eval ((r1 + r2),x) by A12, A28, FUNCT_1:2
.= (Ext_eval (r1,x)) + (Ext_eval (r2,x)) by A0, FIELD_11:19
.= a + c by FIELD_6:15 ;
hence Ext_eval (p,x) in the carrier of (RAdj (F,T)) ; :: thesis:

end;

A36: S₁[ 0 ]

proof

let p be Polynomial of (card T),F; :: thesis:
assume card (Support p) = 0 ; :: thesis:
then Support p = {} ;
then p = 0_ ((card T),F) by FIELD_11:5;
then Ext_eval (p,x) = 0. E by FIELD_11:16
.= 0. (RAdj (F,T)) by FIELD_6:def 4 ;
hence Ext_eval (p,x) in the carrier of (RAdj (F,T)) ; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A36, A2);
hence Ext_eval (p,x) in the carrier of (RAdj (F,T)) by A1; :: thesis: