let F be Field; :: thesis: for E being FieldExtension of F
for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let E be FieldExtension of F; :: thesis: for K being F -extending FieldExtension of F
for h being F -fixing Monomorphism of E,K
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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let K be F -extending FieldExtension of F; :: thesis: for h being F -fixing Monomorphism of E,K
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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let h be F -fixing Monomorphism of E,K; :: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let b be bag of card T; :: thesis: for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let x be T -evaluating Function of (card T),E; :: thesis: h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)));
set n = card T;
set R = RAdj (F,(h .: T));
H0: ( 0. K = 0. (RAdj (F,(h .: T))) & 1. K = 1. (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T))) )
assume A0: card (support b) = 0 ; :: thesis: for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let x be T -evaluating Function of (card T),E; :: thesis: h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) = h . (1_ E) by POLYNOM2:14
.= 1_ K by GROUP_1:def 13 ;
hence h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T))) )
assume B0: card (support b) = k + 1 ; :: thesis: for x being T -evaluating Function of (card T),E holds h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T)))
let x be T -evaluating Function of (card T),E; :: thesis: h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 = h . (eval ((b \ a),x)) as Element of (RAdj (F,(h .: 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 = h . (eval ((({a},(b . a)) -bag),x)) as Element of (RAdj (F,(h .: T))) by Lm10;
h . (eval (b,x)) = h . (eval (((b \ a) + (({a},(b . a)) -bag)),x)) by RING_5:30
.= h . ((eval ((b \ a),x)) * (eval ((({a},(b . a)) -bag),x))) by POLYNOM2:16
.= (h . (eval ((b \ a),x))) * (h . (eval ((({a},(b . a)) -bag),x))) by GROUP_6:def 6
.= u * v by FIELD_6:16 ;
hence h . (eval (b,x)) in the carrier of (RAdj (F,(h .: 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 h . (eval (b,x)) in the carrier of (RAdj (F,(h .: T))) by C, D; :: thesis: verum