let n be Ordinal; :: thesis: for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr

for c being ConstPoly of n,L

for x being Function of n,L holds eval (c,x) = coefficient c

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for c being ConstPoly of n,L

for x being Function of n,L holds eval (c,x) = coefficient c

let c be ConstPoly of n,L; :: thesis: for x being Function of n,L holds eval (c,x) = coefficient c

let x be Function of n,L; :: thesis: eval (c,x) = coefficient c

consider y being FinSequence of the carrier of L such that

A1: len y = len (SgmX ((BagOrder n),(Support c))) and

A2: eval (c,x) = Sum y and

A3: for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((c * (SgmX ((BagOrder n),(Support c)))) /. i) * (eval (((SgmX ((BagOrder n),(Support c))) /. i),x)) by POLYNOM2:def 4;

for c being ConstPoly of n,L

for x being Function of n,L holds eval (c,x) = coefficient c

let L be non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for c being ConstPoly of n,L

for x being Function of n,L holds eval (c,x) = coefficient c

let c be ConstPoly of n,L; :: thesis: for x being Function of n,L holds eval (c,x) = coefficient c

let x be Function of n,L; :: thesis: eval (c,x) = coefficient c

consider y being FinSequence of the carrier of L such that

A1: len y = len (SgmX ((BagOrder n),(Support c))) and

A2: eval (c,x) = Sum y and

A3: for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = ((c * (SgmX ((BagOrder n),(Support c)))) /. i) * (eval (((SgmX ((BagOrder n),(Support c))) /. i),x)) by POLYNOM2:def 4;

now :: thesis: ( ( coefficient c = 0. L & eval (c,x) = coefficient c ) or ( coefficient c <> 0. L & eval (c,x) = coefficient c ) )end;

hence
eval (c,x) = coefficient c
; :: thesis: verumper cases
( coefficient c = 0. L or coefficient c <> 0. L )
;

end;

case A4:
coefficient c = 0. L
; :: thesis: eval (c,x) = coefficient c

Support c = {}

SgmX ((BagOrder n),Sc) = {} by POLYNOM2:18, PRE_POLY:76;

then y = <*> the carrier of L by A1;

hence eval (c,x) = coefficient c by A2, A4, RLVECT_1:43; :: thesis: verum

end;proof

then reconsider Sc = Support c as empty Subset of (Bags n) ;
set u = the Element of Support c;

assume A5: Support c <> {} ; :: thesis: contradiction

then the Element of Support c in Support c ;

then reconsider u = the Element of Support c as Element of Bags n ;

c . u <> 0. L by A5, POLYNOM1:def 4;

then u <> EmptyBag n by A4, Lm2;

then c . u = 0. L by Def7;

hence contradiction by A5, POLYNOM1:def 4; :: thesis: verum

end;assume A5: Support c <> {} ; :: thesis: contradiction

then the Element of Support c in Support c ;

then reconsider u = the Element of Support c as Element of Bags n ;

c . u <> 0. L by A5, POLYNOM1:def 4;

then u <> EmptyBag n by A4, Lm2;

then c . u = 0. L by Def7;

hence contradiction by A5, POLYNOM1:def 4; :: thesis: verum

SgmX ((BagOrder n),Sc) = {} by POLYNOM2:18, PRE_POLY:76;

then y = <*> the carrier of L by A1;

hence eval (c,x) = coefficient c by A2, A4, RLVECT_1:43; :: thesis: verum

case A6:
coefficient c <> 0. L
; :: thesis: eval (c,x) = coefficient c

reconsider sc = Support c as finite Subset of (Bags n) ;

set sg = SgmX ((BagOrder n),sc);

A7: BagOrder n linearly_orders sc by POLYNOM2:18;

A8: for u being object st u in Support c holds

u in {(EmptyBag n)}

u in Support c

then A13: rng (SgmX ((BagOrder n),sc)) = {(EmptyBag n)} by A7, PRE_POLY:def 2;

then A14: EmptyBag n in rng (SgmX ((BagOrder n),sc)) by TARSKI:def 1;

then A15: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_3:31;

then A16: (SgmX ((BagOrder n),sc)) . 1 in rng (SgmX ((BagOrder n),sc)) by FUNCT_1:3;

A17: for u being object st u in dom (SgmX ((BagOrder n),sc)) holds

u in {1}

u in dom (SgmX ((BagOrder n),sc)) by A15, TARSKI:def 1;

then A24: dom (SgmX ((BagOrder n),sc)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:2;

then A25: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_1:2, TARSKI:def 1;

(SgmX ((BagOrder n),sc)) /. 1 = (SgmX ((BagOrder n),sc)) . 1 by A15, PARTFUN1:def 6;

then (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A25, FUNCT_1:3;

then A26: (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def 1;

A27: len (SgmX ((BagOrder n),sc)) = 1 by A24, FINSEQ_1:def 3;

dom c = Bags n by FUNCT_2:def 1;

then 1 in dom (c * (SgmX ((BagOrder n),sc))) by A13, A15, A16, FUNCT_1:11;

then A28: (c * (SgmX ((BagOrder n),sc))) /. 1 = (c * (SgmX ((BagOrder n),sc))) . 1 by PARTFUN1:def 6

.= c . ((SgmX ((BagOrder n),sc)) . 1) by A15, FUNCT_1:13

.= c . (EmptyBag n) by A13, A16, TARSKI:def 1

.= coefficient c by Lm2 ;

dom y = Seg (len y) by FINSEQ_1:def 3

.= dom (SgmX ((BagOrder n),sc)) by A1, FINSEQ_1:def 3 ;

then y . 1 = y /. 1 by A25, PARTFUN1:def 6

.= (coefficient c) * (eval ((EmptyBag n),x)) by A1, A3, A27, A26, A28

.= (coefficient c) * (1. L) by POLYNOM2:14

.= coefficient c ;

then y = <*(coefficient c)*> by A1, A27, FINSEQ_1:40;

hence eval (c,x) = coefficient c by A2, RLVECT_1:44; :: thesis: verum

end;set sg = SgmX ((BagOrder n),sc);

A7: BagOrder n linearly_orders sc by POLYNOM2:18;

A8: for u being object st u in Support c holds

u in {(EmptyBag n)}

proof

for u being object st u in {(EmptyBag n)} holds
let u be object ; :: thesis: ( u in Support c implies u in {(EmptyBag n)} )

assume A9: u in Support c ; :: thesis: u in {(EmptyBag n)}

assume A10: not u in {(EmptyBag n)} ; :: thesis: contradiction

reconsider u = u as Element of Bags n by A9;

u <> EmptyBag n by A10, TARSKI:def 1;

then c . u = 0. L by Def7;

hence contradiction by A9, POLYNOM1:def 4; :: thesis: verum

end;assume A9: u in Support c ; :: thesis: u in {(EmptyBag n)}

assume A10: not u in {(EmptyBag n)} ; :: thesis: contradiction

reconsider u = u as Element of Bags n by A9;

u <> EmptyBag n by A10, TARSKI:def 1;

then c . u = 0. L by Def7;

hence contradiction by A9, POLYNOM1:def 4; :: thesis: verum

u in Support c

proof

then
Support c = {(EmptyBag n)}
by A8, TARSKI:2;
let u be object ; :: thesis: ( u in {(EmptyBag n)} implies u in Support c )

assume A11: u in {(EmptyBag n)} ; :: thesis: u in Support c

then A12: u = EmptyBag n by TARSKI:def 1;

reconsider u = u as Element of Bags n by A11;

c . u <> 0. L by A6, A12, Lm2;

hence u in Support c by POLYNOM1:def 4; :: thesis: verum

end;assume A11: u in {(EmptyBag n)} ; :: thesis: u in Support c

then A12: u = EmptyBag n by TARSKI:def 1;

reconsider u = u as Element of Bags n by A11;

c . u <> 0. L by A6, A12, Lm2;

hence u in Support c by POLYNOM1:def 4; :: thesis: verum

then A13: rng (SgmX ((BagOrder n),sc)) = {(EmptyBag n)} by A7, PRE_POLY:def 2;

then A14: EmptyBag n in rng (SgmX ((BagOrder n),sc)) by TARSKI:def 1;

then A15: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_3:31;

then A16: (SgmX ((BagOrder n),sc)) . 1 in rng (SgmX ((BagOrder n),sc)) by FUNCT_1:3;

A17: for u being object st u in dom (SgmX ((BagOrder n),sc)) holds

u in {1}

proof

for u being object st u in {1} holds
let u be object ; :: thesis: ( u in dom (SgmX ((BagOrder n),sc)) implies u in {1} )

assume A18: u in dom (SgmX ((BagOrder n),sc)) ; :: thesis: u in {1}

assume A19: not u in {1} ; :: thesis: contradiction

reconsider u = u as Element of NAT by A18;

(SgmX ((BagOrder n),sc)) /. u = (SgmX ((BagOrder n),sc)) . u by A18, PARTFUN1:def 6;

then A20: (SgmX ((BagOrder n),sc)) /. u in rng (SgmX ((BagOrder n),sc)) by A18, FUNCT_1:3;

A21: u <> 1 by A19, TARSKI:def 1;

A22: 1 < u

then (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A15, FUNCT_1:3;

then (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def 1

.= (SgmX ((BagOrder n),sc)) /. u by A13, A20, TARSKI:def 1 ;

hence contradiction by A7, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum

end;assume A18: u in dom (SgmX ((BagOrder n),sc)) ; :: thesis: u in {1}

assume A19: not u in {1} ; :: thesis: contradiction

reconsider u = u as Element of NAT by A18;

(SgmX ((BagOrder n),sc)) /. u = (SgmX ((BagOrder n),sc)) . u by A18, PARTFUN1:def 6;

then A20: (SgmX ((BagOrder n),sc)) /. u in rng (SgmX ((BagOrder n),sc)) by A18, FUNCT_1:3;

A21: u <> 1 by A19, TARSKI:def 1;

A22: 1 < u

proof

(SgmX ((BagOrder n),sc)) /. 1 = (SgmX ((BagOrder n),sc)) . 1
by A14, A18, FINSEQ_3:31, PARTFUN1:def 6;
consider k being Nat such that

A23: dom (SgmX ((BagOrder n),sc)) = Seg k by FINSEQ_1:def 2;

Seg k = { m where m is Nat : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;

then ex m9 being Nat st

( m9 = u & 1 <= m9 & m9 <= k ) by A18, A23;

hence 1 < u by A21, XXREAL_0:1; :: thesis: verum

end;A23: dom (SgmX ((BagOrder n),sc)) = Seg k by FINSEQ_1:def 2;

Seg k = { m where m is Nat : ( 1 <= m & m <= k ) } by FINSEQ_1:def 1;

then ex m9 being Nat st

( m9 = u & 1 <= m9 & m9 <= k ) by A18, A23;

hence 1 < u by A21, XXREAL_0:1; :: thesis: verum

then (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A15, FUNCT_1:3;

then (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def 1

.= (SgmX ((BagOrder n),sc)) /. u by A13, A20, TARSKI:def 1 ;

hence contradiction by A7, A15, A18, A22, PRE_POLY:def 2; :: thesis: verum

u in dom (SgmX ((BagOrder n),sc)) by A15, TARSKI:def 1;

then A24: dom (SgmX ((BagOrder n),sc)) = Seg 1 by A17, FINSEQ_1:2, TARSKI:2;

then A25: 1 in dom (SgmX ((BagOrder n),sc)) by FINSEQ_1:2, TARSKI:def 1;

(SgmX ((BagOrder n),sc)) /. 1 = (SgmX ((BagOrder n),sc)) . 1 by A15, PARTFUN1:def 6;

then (SgmX ((BagOrder n),sc)) /. 1 in rng (SgmX ((BagOrder n),sc)) by A25, FUNCT_1:3;

then A26: (SgmX ((BagOrder n),sc)) /. 1 = EmptyBag n by A13, TARSKI:def 1;

A27: len (SgmX ((BagOrder n),sc)) = 1 by A24, FINSEQ_1:def 3;

dom c = Bags n by FUNCT_2:def 1;

then 1 in dom (c * (SgmX ((BagOrder n),sc))) by A13, A15, A16, FUNCT_1:11;

then A28: (c * (SgmX ((BagOrder n),sc))) /. 1 = (c * (SgmX ((BagOrder n),sc))) . 1 by PARTFUN1:def 6

.= c . ((SgmX ((BagOrder n),sc)) . 1) by A15, FUNCT_1:13

.= c . (EmptyBag n) by A13, A16, TARSKI:def 1

.= coefficient c by Lm2 ;

dom y = Seg (len y) by FINSEQ_1:def 3

.= dom (SgmX ((BagOrder n),sc)) by A1, FINSEQ_1:def 3 ;

then y . 1 = y /. 1 by A25, PARTFUN1:def 6

.= (coefficient c) * (eval ((EmptyBag n),x)) by A1, A3, A27, A26, A28

.= (coefficient c) * (1. L) by POLYNOM2:14

.= coefficient c ;

then y = <*(coefficient c)*> by A1, A27, FINSEQ_1:40;

hence eval (c,x) = coefficient c by A2, RLVECT_1:44; :: thesis: verum