let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of {} ,L
for x being Function of {} ,L holds eval p,x = p . (EmptyBag {} )
let p be Polynomial of {} ,L; :: thesis: for x being Function of {} ,L holds eval p,x = p . (EmptyBag {} )
let x be Function of {} ,L; :: thesis: eval p,x = p . (EmptyBag {} )
set n = {} ;
A1: for b being bag of holds b = {}

proof

let b be bag of ; :: thesis: b = {}
b in Bags {} by POLYNOM1:def 14;
hence b = {} by POLYNOM1:55, TARSKI:def 1; :: thesis: verum

end;

then A2: EmptyBag {} = {} ;
consider a being Element of L such that
A3: p = {(EmptyBag {} )} --> a by Lm1;
A4: dom p = {(EmptyBag {} )} by A3, FUNCOP_1:19;
A5: EmptyBag {} in {(EmptyBag {} )} by TARSKI:def 1;
then A6: p . (EmptyBag {} ) = a by A3, FUNCOP_1:13;

now

per cases ( a = 0. L or a <> 0. L ) ;

case A7: a = 0. L ; :: thesis: eval p,x = a

Support p = {}

proof

assume A8: Support p <> {} ; :: thesis: contradiction
consider u being Element of Support p;
u in Support p by A8;
then reconsider u = u as Element of Bags {} ;
p . u <> 0. L by A8, POLYNOM1:def 9;
hence contradiction by A1, A2, A6, A7; :: thesis: verum

end;

then reconsider Sp = Support p as empty Subset of (Bags {} ) ;
A9: SgmX (BagOrder {} ),Sp = {} by POLYNOM2:9, POLYNOM2:20;
consider y being FinSequence of the carrier of L such that
A10: ( len y = len (SgmX (BagOrder {} ),(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 {} ),(Support p))) /. i) * (eval (((SgmX (BagOrder {} ),(Support p)) /. i) @ ),x) ) ) by POLYNOM2:def 4;
len y = 0 by A9, A10;
then y = <*> the carrier of L ;
hence eval p,x = a by A7, A10, RLVECT_1:60; :: thesis: verum

end;

case A11: a <> 0. L ; :: thesis: eval p,x = a

A12: for u being set st u in Support p holds
u in {{} }

proof

let u be set ; :: thesis: ( u in Support p implies u in {{} } )
assume u in Support p ; :: thesis: u in {{} }
then reconsider u = u as Element of Bags {} ;
u = {} by A1;
hence u in {{} } by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {{} } holds
u in Support p

proof

let u be set ; :: thesis: ( u in {{} } implies u in Support p )
assume u in {{} } ; :: thesis: u in Support p
then u = EmptyBag {} by A2, TARSKI:def 1;
hence u in Support p by A6, A11, POLYNOM1:def 9; :: thesis: verum

end;

then A13: Support p = {{} } by A12, TARSKI:2;
reconsider sp = Support p as finite Subset of (Bags {} ) ;
set sg = SgmX (BagOrder {} ),sp;
A14: BagOrder {} linearly_orders sp by POLYNOM2:20;
then A15: ( rng (SgmX (BagOrder {} ),sp) = {{} } & ( for l, m being Nat st l in dom (SgmX (BagOrder {} ),sp) & m in dom (SgmX (BagOrder {} ),sp) & l < m holds
( (SgmX (BagOrder {} ),sp) /. l <> (SgmX (BagOrder {} ),sp) /. m & [((SgmX (BagOrder {} ),sp) /. l),((SgmX (BagOrder {} ),sp) /. m)] in BagOrder {} ) ) ) by A13, TRIANG_1:def 2;
then A16: {} in rng (SgmX (BagOrder {} ),sp) by TARSKI:def 1;
then A17: 1 in dom (SgmX (BagOrder {} ),sp) by FINSEQ_3:33;
then A18: for u being set st u in {1} holds
u in dom (SgmX (BagOrder {} ),sp) by TARSKI:def 1;
for u being set st u in dom (SgmX (BagOrder {} ),sp) holds
u in {1}

proof

let u be set ; :: thesis: ( u in dom (SgmX (BagOrder {} ),sp) implies u in {1} )
assume A19: u in dom (SgmX (BagOrder {} ),sp) ; :: thesis: u in {1}
assume A20: not u in {1} ; :: thesis: contradiction
reconsider u = u as Element of NAT by A19;
A21: u <> 1 by A20, TARSKI:def 1;
A22: 1 < u

proof

consider k being Nat such that
A23: dom (SgmX (BagOrder {} ),sp) = Seg k by FINSEQ_1:def 2;
Seg k = { m where m is Element of NAT : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;
then consider m' being Element of NAT such that
A24: ( m' = u & 1 <= m' & m' <= k ) by A19, A23;
thus 1 < u by A21, A24, XXREAL_0:1; :: thesis: verum

end;

( (SgmX (BagOrder {} ),sp) /. 1 = (SgmX (BagOrder {} ),sp) . 1 & (SgmX (BagOrder {} ),sp) /. u = (SgmX (BagOrder {} ),sp) . u ) by A16, A19, FINSEQ_3:33, PARTFUN1:def 8;
then A25: ( (SgmX (BagOrder {} ),sp) /. 1 in rng (SgmX (BagOrder {} ),sp) & (SgmX (BagOrder {} ),sp) /. u in rng (SgmX (BagOrder {} ),sp) ) by A17, A19, FUNCT_1:12;
then (SgmX (BagOrder {} ),sp) /. 1 = {} by A15, TARSKI:def 1
.= (SgmX (BagOrder {} ),sp) /. u by A15, A25, TARSKI:def 1 ;
hence contradiction by A14, A17, A19, A22, TRIANG_1:def 2; :: thesis: verum

end;

then dom (SgmX (BagOrder {} ),sp) = Seg 1 by A18, FINSEQ_1:4, TARSKI:2;
then A26: len (SgmX (BagOrder {} ),sp) = 1 by FINSEQ_1:def 3;
consider y being FinSequence of the carrier of L such that
A27: ( len y = len (SgmX (BagOrder {} ),sp) & Sum y = eval p,x & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX (BagOrder {} ),sp)) /. i) * (eval (((SgmX (BagOrder {} ),sp) /. i) @ ),x) ) ) by POLYNOM2:def 4;
A28: (SgmX (BagOrder {} ),sp) . 1 in rng (SgmX (BagOrder {} ),sp) by A17, FUNCT_1:12;
(SgmX (BagOrder {} ),sp) . 1 in dom p by A2, A4, A15, A17, FUNCT_1:12;
then 1 in dom (p * (SgmX (BagOrder {} ),sp)) by A17, FUNCT_1:21;
then A29: (p * (SgmX (BagOrder {} ),sp)) /. 1 = (p * (SgmX (BagOrder {} ),sp)) . 1 by PARTFUN1:def 8
.= p . ((SgmX (BagOrder {} ),sp) . 1) by A17, FUNCT_1:23
.= a by A2, A3, A15, A28, FUNCOP_1:13 ;
dom y = Seg (len y) by FINSEQ_1:def 3
.= dom (SgmX (BagOrder {} ),sp) by A27, FINSEQ_1:def 3 ;
then y . 1 = y /. 1 by A16, FINSEQ_3:33, PARTFUN1:def 8
.= ((p * (SgmX (BagOrder {} ),sp)) /. 1) * (eval (((SgmX (BagOrder {} ),sp) /. 1) @ ),x) by A26, A27
.= ((p * (SgmX (BagOrder {} ),sp)) /. 1) * (eval (EmptyBag {} ),x) by A1, A2
.= ((p * (SgmX (BagOrder {} ),sp)) /. 1) * (1. L) by POLYNOM2:16
.= a by A29, VECTSP_1:def 13 ;
then y = <*a*> by A26, A27, FINSEQ_1:57;
hence eval p,x = a by A27, RLVECT_1:61; :: thesis: verum

end;

end;

end;

hence eval p,x = p . (EmptyBag {} ) by A3, A5, FUNCOP_1:13; :: thesis: verum