let n be Ordinal; :: thesis: for L being non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for b being bag of st Support p = {b} holds
for x being Function of n,L holds eval p,x = (p . b) * (eval b,x)
let L be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for b being bag of st Support p = {b} holds
for x being Function of n,L holds eval p,x = (p . b) * (eval b,x)
let p be Polynomial of n,L; :: thesis: for b being bag of st Support p = {b} holds
for x being Function of n,L holds eval p,x = (p . b) * (eval b,x)
let b be bag of ; :: thesis: ( Support p = {b} implies for x being Function of n,L holds eval p,x = (p . b) * (eval b,x) )
assume A1: Support p = {b} ; :: thesis: for x being Function of n,L holds eval p,x = (p . b) * (eval b,x)
let x be Function of n,L; :: thesis: eval p,x = (p . b) * (eval b,x)
consider y being FinSequence of the carrier of L such that
A2: ( len y = len (SgmX (BagOrder n),(Support p)) & eval p,x = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder n),(Support p))) /. i) * (eval (((SgmX (BagOrder n),(Support p)) /. i) @ ),x) ) ) by Def4;
reconsider sp = Support p as finite Subset of (Bags n) ;
set sg = SgmX (BagOrder n),sp;
A3: BagOrder n linearly_orders sp by Th20;
then A4: ( rng (SgmX (BagOrder n),sp) = {b} & ( for l, m being Element of NAT st l in dom (SgmX (BagOrder n),sp) & m in dom (SgmX (BagOrder n),sp) & l < m holds
( (SgmX (BagOrder n),sp) /. l <> (SgmX (BagOrder n),sp) /. m & [((SgmX (BagOrder n),sp) /. l),((SgmX (BagOrder n),sp) /. m)] in BagOrder n ) ) ) by A1, TRIANG_1: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:33;
then A7: for u being set st u in {1} holds
u in dom (SgmX (BagOrder n),sp) by TARSKI:def 1;
for u being set st u in dom (SgmX (BagOrder n),sp) holds
u in {1}

proof

let u be set ; :: thesis: ( u in dom (SgmX (BagOrder n),sp) implies u in {1} )
assume A8: u in dom (SgmX (BagOrder n),sp) ; :: thesis: u in {1}
assume A9: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A8;
A10: u <> 1 by A9, TARSKI:def 1;
A11: 1 < u

proof

consider k being Nat such that
A12: dom (SgmX (BagOrder n),sp) = Seg k by FINSEQ_1:def 2;
Seg k = { l where l is Element of NAT : ( 1 <= l & l <= k ) } by FINSEQ_1:def 1;
then consider m' being Element of NAT such that
A13: ( m' = u & 1 <= m' & m' <= k ) by A8, A12;
thus 1 < u by A10, A13, XXREAL_0:1; :: thesis: verum

end;

( (SgmX (BagOrder n),sp) /. 1 = (SgmX (BagOrder n),sp) . 1 & (SgmX (BagOrder n),sp) /. u = (SgmX (BagOrder n),sp) . u ) by A5, A8, FINSEQ_3:33, PARTFUN1:def 8;
then A14: ( (SgmX (BagOrder n),sp) /. 1 in rng (SgmX (BagOrder n),sp) & (SgmX (BagOrder n),sp) /. u in rng (SgmX (BagOrder n),sp) ) by A6, A8, FUNCT_1:def 5;
then (SgmX (BagOrder n),sp) /. 1 = b by A4, TARSKI:def 1
.= (SgmX (BagOrder n),sp) /. u by A4, A14, TARSKI:def 1 ;
hence contradiction by A3, A6, A8, A11, TRIANG_1:def 2; :: thesis: verum

end;

then A15: dom (SgmX (BagOrder n),sp) = Seg 1 by A7, FINSEQ_1:4, TARSKI:2;
then A16: len (SgmX (BagOrder n),sp) = 1 by FINSEQ_1:def 3;
A17: 1 in dom (SgmX (BagOrder n),sp) by A15, FINSEQ_1:4, TARSKI:def 1;
(SgmX (BagOrder n),sp) /. 1 = (SgmX (BagOrder n),sp) . 1 by A6, PARTFUN1:def 8;
then A18: (SgmX (BagOrder n),sp) /. 1 in rng (SgmX (BagOrder n),sp) by A17, FUNCT_1:def 5;
A19: y . 1 = y /. 1 by A2, A16, FINSEQ_4:24
.= ((p * (SgmX (BagOrder n),sp)) /. 1) * (eval (((SgmX (BagOrder n),sp) /. 1) @ ),x) by A2, A16
.= ((p * (SgmX (BagOrder n),sp)) /. 1) * (eval b,x) by A4, A18, TARSKI:def 1 ;
A20: (SgmX (BagOrder n),sp) . 1 in rng (SgmX (BagOrder n),sp) by A6, FUNCT_1:def 5;
then A21: (SgmX (BagOrder n),sp) . 1 = b by A4, TARSKI:def 1;
A22: b in Bags n by POLYNOM1:def 14;
dom p = Bags n by FUNCT_2:def 1;
then 1 in dom (p * (SgmX (BagOrder n),sp)) by A6, A21, A22, FUNCT_1:21;
then (p * (SgmX (BagOrder n),sp)) /. 1 = (p * (SgmX (BagOrder n),sp)) . 1 by PARTFUN1:def 8
.= p . ((SgmX (BagOrder n),sp) . 1) by A6, FUNCT_1:23
.= p . b by A4, A20, TARSKI:def 1 ;
then y = <*((p . b) * (eval b,x))*> by A2, A16, A19, FINSEQ_1:57;
hence eval p,x = (p . b) * (eval b,x) by A2, RLVECT_1:61; :: thesis: verum