let n be Ordinal; for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for b being bag of n 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 trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; for p being Polynomial of n,L
for b being bag of n 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; for b being bag of n 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 n; ( Support p = {b} implies for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x)) )
reconsider sp = Support p as finite Subset of (Bags n) ;
set sg = SgmX ((BagOrder n),sp);
A1:
b in Bags n
by PRE_POLY:def 12;
A2:
dom p = Bags n
by FUNCT_2:def 1;
A3:
BagOrder n linearly_orders sp
by Th10;
assume
Support p = {b}
; for x being Function of n,L holds eval (p,x) = (p . b) * (eval (b,x))
then A4:
rng (SgmX ((BagOrder n),sp)) = {b}
by 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 ;
( u in dom (SgmX ((BagOrder n),sp)) implies u in {1} )
assume A9:
u in dom (SgmX ((BagOrder n),sp))
;
u in {1}
assume A10:
not
u in {1}
;
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
(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;
verum
end;
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;
then A16:
len (SgmX ((BagOrder n),sp)) = 1
by FINSEQ_1:def 3;
A17:
(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;
then
1 in dom (p * (SgmX ((BagOrder n),sp)))
by A6, A1, A2, FUNCT_1:11;
then A18: (p * (SgmX ((BagOrder n),sp))) /. 1 =
(p * (SgmX ((BagOrder n),sp))) . 1
by PARTFUN1:def 6
.=
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, FINSEQ_1:2, TARSKI:def 1;
then A19:
(SgmX ((BagOrder n),sp)) /. 1 in rng (SgmX ((BagOrder n),sp))
by A7, FUNCT_1:def 3;
let x be Function of n,L; eval (p,x) = (p . b) * (eval (b,x))
consider y being FinSequence of the carrier of L such that
A20:
len y = len (SgmX ((BagOrder n),(Support p)))
and
A21:
eval (p,x) = Sum y
and
A22:
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 Def2;
y . 1 =
y /. 1
by A20, A16, FINSEQ_4:15
.=
((p * (SgmX ((BagOrder n),sp))) /. 1) * (eval (((SgmX ((BagOrder n),sp)) /. 1),x))
by A20, A22, A16
.=
((p * (SgmX ((BagOrder n),sp))) /. 1) * (eval (b,x))
by A4, A19, TARSKI:def 1
;
then
y = <*((p . b) * (eval (b,x)))*>
by A20, A16, A18, FINSEQ_1:40;
hence
eval (p,x) = (p . b) * (eval (b,x))
by A21, RLVECT_1:44; verum