let R, S be non degenerated comRing; :: thesis: for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st Support p = {b} holds
for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))
let n be Ordinal; :: thesis: for p being Polynomial of n,R
for b being bag of n st Support p = {b} holds
for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))
let p be Polynomial of n,R; :: thesis: for b being bag of n st Support p = {b} holds
for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))
let b be bag of n; :: thesis: ( Support p = {b} implies for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x)) )
assume A0: Support p = {b} ; :: thesis: for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))
let x be Function of n,S; :: thesis: Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))
reconsider sp = Support p as finite Subset of (Bags n) ;
set sg = SgmX ((BagOrder n),sp);
A3: BagOrder n linearly_orders sp by POLYNOM2:18;
A4: rng (SgmX ((BagOrder n),sp)) = {b} by A0, A3, PRE_POLY:def 2;
then A5: b in rng (SgmX ((BagOrder n),sp)) by TARSKI:def 1;
then A6: 1 in dom (SgmX ((BagOrder n),sp)) by FINSEQ_3:31;
then A7: (SgmX ((BagOrder n),sp)) /. 1 = (SgmX ((BagOrder n),sp)) . 1 by PARTFUN1:def 6;
A8: for u being object st u in dom (SgmX ((BagOrder n),sp)) holds
u in {1}

proof

let u be object ; :: thesis: ( u in dom (SgmX ((BagOrder n),sp)) implies u in {1} )
assume A9: u in dom (SgmX ((BagOrder n),sp)) ; :: thesis: u in {1}
assume A10: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A9;
(SgmX ((BagOrder n),sp)) /. u = (SgmX ((BagOrder n),sp)) . u by A9, PARTFUN1:def 6;
then A11: (SgmX ((BagOrder n),sp)) /. u in rng (SgmX ((BagOrder n),sp)) by A9, FUNCT_1:def 3;
A12: u <> 1 by A10, TARSKI:def 1;
A13: 1 < u

proof

consider k being Nat such that
A14: dom (SgmX ((BagOrder n),sp)) = Seg k by FINSEQ_1:def 2;
ex m9 being Nat st
( m9 = u & 1 <= m9 & m9 <= k ) by A9, A14;
hence 1 < u by A12, XXREAL_0:1; :: thesis: verum

end;

(SgmX ((BagOrder n),sp)) /. 1 = (SgmX ((BagOrder n),sp)) . 1 by A5, A9, FINSEQ_3:31, PARTFUN1:def 6;
then (SgmX ((BagOrder n),sp)) /. 1 in rng (SgmX ((BagOrder n),sp)) by A6, FUNCT_1:def 3;
then (SgmX ((BagOrder n),sp)) /. 1 = b by A4, TARSKI:def 1
.= (SgmX ((BagOrder n),sp)) /. u by A4, A11, TARSKI:def 1 ;
hence contradiction by A3, A6, A9, A13, PRE_POLY:def 2; :: thesis: verum

end;

Z: for u being object st u in {1} holds
u in dom (SgmX ((BagOrder n),sp)) by A6, TARSKI:def 1;
then A15: dom (SgmX ((BagOrder n),sp)) = Seg 1 by A8, FINSEQ_1:2, TARSKI:2;
A16: len (SgmX ((BagOrder n),sp)) = 1 by Z, A8, FINSEQ_1:2, TARSKI:2, FINSEQ_1:def 3;
A17: (SgmX ((BagOrder n),sp)) . 1 in rng (SgmX ((BagOrder n),sp)) by A6, FUNCT_1:def 3;
A18: (p * (SgmX ((BagOrder n),sp))) . 1 = p . ((SgmX ((BagOrder n),sp)) . 1) by A6, FUNCT_1:13
.= p . b by A4, A17, TARSKI:def 1 ;
1 in dom (SgmX ((BagOrder n),sp)) by A15;
then A19: (SgmX ((BagOrder n),sp)) /. 1 in rng (SgmX ((BagOrder n),sp)) by A7, FUNCT_1:def 3;
consider y being FinSequence of the carrier of S such that
A21: Ext_eval (p,x) = Sum y and
A20: len y = len (SgmX ((BagOrder n),(Support p))) and
A22: for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),sp))) . i),S)) * (eval (((SgmX ((BagOrder n),sp)) /. i),x)) by defeval;
y . 1 = (In (((p * (SgmX ((BagOrder n),sp))) . 1),S)) * (eval (((SgmX ((BagOrder n),sp)) /. 1),x)) by A20, A22, A16
.= (In (((p * (SgmX ((BagOrder n),sp))) . 1),S)) * (eval (b,x)) by A4, A19, TARSKI:def 1 ;
then y = <*((In ((p . b),S)) * (eval (b,x)))*> by A20, A16, A18, FINSEQ_1:40;
hence Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x)) by A21, RLVECT_1:44; :: thesis: verum