let F be Field; :: thesis: for E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of card T
for x being b₂ -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let E be FieldExtension of F; :: thesis: for T being non empty finite Subset of E
for b being bag of card T
for x being b₁ -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let T be non empty finite Subset of E; :: thesis: for b being bag of card T
for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let b be bag of card T; :: thesis: for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: eval (b,x) in the carrier of (RAdj (F,T))
defpred S₁[ Nat] means for b being bag of card T st card (support b) = $1 holds
for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T));
set n = card T;
set R = RAdj (F,T);
H0: ( 0. E = 0. (RAdj (F,T)) & 1. E = 1. (RAdj (F,T)) ) by FIELD_6:def 4;
A: S₁[ 0 ]

proof

now :: thesis: for b being bag of card T st card (support b) = 0 holds
for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))

let b be bag of card T; :: thesis: ( card (support b) = 0 implies for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T)) )
assume A0: card (support b) = 0 ; :: thesis: for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: eval (b,x) in the carrier of (RAdj (F,T))

now :: thesis: for o being object st o in card T holds
b . o = (EmptyBag (card T)) . o

let o be object ; :: thesis: ( o in card T implies b . o = (EmptyBag (card T)) . o )
assume o in card T ; :: thesis: b . o = (EmptyBag (card T)) . o
not o in support b by A0;
hence b . o = {} by PRE_POLY:def 7
.= (EmptyBag (card T)) . o by PBOOLE:5 ;
:: thesis: verum

end;

then b = EmptyBag (card T) by PBOOLE:def 10;
then eval (b,x) = 1. E by POLYNOM2:14;
hence eval (b,x) in the carrier of (RAdj (F,T)) by H0; :: thesis: verum

end;

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

end;

B: 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 b being bag of card T st card (support b) = k + 1 holds
for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))

let b be bag of card T; :: thesis: ( card (support b) = k + 1 implies for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T)) )
assume B0: card (support b) = k + 1 ; :: thesis: for x being T -evaluating Function of (card T),E holds eval (b,x) in the carrier of (RAdj (F,T))
let x be T -evaluating Function of (card T),E; :: thesis: eval (b,x) in the carrier of (RAdj (F,T))
set a = the Element of support b;
B3: support b <> {} by B0;
then B1: ( the Element of support b in support b & support b c= dom b & dom b c= card T ) by PRE_POLY:37;
then reconsider a = the Element of support b as Element of card T ;
set b1 = b \ a;
set b2 = ({a},(b . a)) -bag ;
B2: support (b \ a) = (support b) \ {a} by RING_5:29;
{a} c= support b by B1, TARSKI:def 1;
then card (support (b \ a)) = (card (support b)) - (card {a}) by B2, CARD_2:44
.= (k + 1) - 1 by B0, CARD_2:42 ;
then reconsider u = eval ((b \ a),x) as Element of (RAdj (F,T)) by IV;
b . a <> 0 by B3, PRE_POLY:def 7;
then support (({a},(b . a)) -bag) = {a} by UPROOTS:8;
then reconsider v = eval ((({a},(b . a)) -bag),x) as Element of (RAdj (F,T)) by lemphi2ax;
eval (b,x) = eval (((b \ a) + (({a},(b . a)) -bag)),x) by RING_5:30
.= (eval ((b \ a),x)) * (eval ((({a},(b . a)) -bag),x)) by POLYNOM2:16
.= u * v by FIELD_6:16 ;
hence eval (b,x) in the carrier of (RAdj (F,T)) ; :: thesis: verum

end;

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

end;

C: for k being Nat holds S₁[k] from NAT_1:sch 2(A, B);
consider n being Nat such that
D: card (support b) = n ;
thus eval (b,x) in the carrier of (RAdj (F,T)) by C, D; :: thesis: verum