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

for m being Monomial of n,L

for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

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

for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

let m be Monomial of n,L; :: thesis: for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

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

consider y being FinSequence of the carrier of L such that

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

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

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

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

consider b being bag of n such that

A4: for b9 being bag of n st b9 <> b holds

m . b9 = 0. L by Def3;

for m being Monomial of n,L

for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

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

for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

let m be Monomial of n,L; :: thesis: for x being Function of n,L holds eval (m,x) = (coefficient m) * (eval ((term m),x))

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

consider y being FinSequence of the carrier of L such that

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

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

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

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

consider b being bag of n such that

A4: for b9 being bag of n st b9 <> b holds

m . b9 = 0. L by Def3;

now :: thesis: ( ( m . b <> 0. L & eval (m,x) = (coefficient m) * (eval ((term m),x)) ) or ( m . b = 0. L & eval (m,x) = (coefficient m) * (eval ((term m),x)) ) )end;

hence
eval (m,x) = (coefficient m) * (eval ((term m),x))
; :: thesis: verumper cases
( m . b <> 0. L or m . b = 0. L )
;

end;

case A5:
m . b <> 0. L
; :: thesis: eval (m,x) = (coefficient m) * (eval ((term m),x))

A6:
for u being object st u in Support m holds

u in {b}

reconsider sm = Support m as finite Subset of (Bags n) ;

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

A10: BagOrder n linearly_orders sm by POLYNOM2:18;

for u being object st u in {b} holds

u in Support m

then A12: rng (SgmX ((BagOrder n),sm)) = {b} by A10, PRE_POLY:def 2;

then A13: b in rng (SgmX ((BagOrder n),sm)) by TARSKI:def 1;

then A14: 1 in dom (SgmX ((BagOrder n),sm)) by FINSEQ_3:31;

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

then (SgmX ((BagOrder n),sm)) . 1 = b by A12, TARSKI:def 1;

then 1 in dom (m * (SgmX ((BagOrder n),sm))) by A14, A9, FUNCT_1:11;

then A16: (m * (SgmX ((BagOrder n),sm))) /. 1 = (m * (SgmX ((BagOrder n),sm))) . 1 by PARTFUN1:def 6

.= m . ((SgmX ((BagOrder n),sm)) . 1) by A14, FUNCT_1:13

.= m . b by A12, A15, TARSKI:def 1

.= coefficient m by A5, Def5 ;

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

u in {1}

u in dom (SgmX ((BagOrder n),sm)) by A14, TARSKI:def 1;

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

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

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

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

then A26: (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def 1;

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

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

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

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

.= ((m * (SgmX ((BagOrder n),sm))) /. 1) * (eval (b,x)) by A26, A1, A3, A27 ;

then y = <*((coefficient m) * (eval (b,x)))*> by A1, A27, A16, FINSEQ_1:40;

hence eval (m,x) = (coefficient m) * (eval (b,x)) by A2, RLVECT_1:44

.= (coefficient m) * (eval ((term m),x)) by A5, Def5 ;

:: thesis: verum

end;u in {b}

proof

A9:
( b in Bags n & dom m = Bags n )
by FUNCT_2:def 1, PRE_POLY:def 12;
let u be object ; :: thesis: ( u in Support m implies u in {b} )

assume A7: u in Support m ; :: thesis: u in {b}

assume A8: not u in {b} ; :: thesis: contradiction

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

u <> b by A8, TARSKI:def 1;

then m . u = 0. L by A4;

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

end;assume A7: u in Support m ; :: thesis: u in {b}

assume A8: not u in {b} ; :: thesis: contradiction

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

u <> b by A8, TARSKI:def 1;

then m . u = 0. L by A4;

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

reconsider sm = Support m as finite Subset of (Bags n) ;

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

A10: BagOrder n linearly_orders sm by POLYNOM2:18;

for u being object st u in {b} holds

u in Support m

proof

then
Support m = {b}
by A6, TARSKI:2;
let u be object ; :: thesis: ( u in {b} implies u in Support m )

assume A11: u in {b} ; :: thesis: u in Support m

then u = b by TARSKI:def 1;

then reconsider u = u as Element of Bags n by PRE_POLY:def 12;

m . u <> 0. L by A5, A11, TARSKI:def 1;

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

end;assume A11: u in {b} ; :: thesis: u in Support m

then u = b by TARSKI:def 1;

then reconsider u = u as Element of Bags n by PRE_POLY:def 12;

m . u <> 0. L by A5, A11, TARSKI:def 1;

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

then A12: rng (SgmX ((BagOrder n),sm)) = {b} by A10, PRE_POLY:def 2;

then A13: b in rng (SgmX ((BagOrder n),sm)) by TARSKI:def 1;

then A14: 1 in dom (SgmX ((BagOrder n),sm)) by FINSEQ_3:31;

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

then (SgmX ((BagOrder n),sm)) . 1 = b by A12, TARSKI:def 1;

then 1 in dom (m * (SgmX ((BagOrder n),sm))) by A14, A9, FUNCT_1:11;

then A16: (m * (SgmX ((BagOrder n),sm))) /. 1 = (m * (SgmX ((BagOrder n),sm))) . 1 by PARTFUN1:def 6

.= m . ((SgmX ((BagOrder n),sm)) . 1) by A14, FUNCT_1:13

.= m . b by A12, A15, TARSKI:def 1

.= coefficient m by A5, Def5 ;

A17: for u being object st u in dom (SgmX ((BagOrder n),sm)) 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),sm)) implies u in {1} )

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

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

reconsider u = u as Element of NAT by A18;

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

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

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

A22: 1 < u

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

then (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def 1

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

hence contradiction by A10, A14, A18, A22, PRE_POLY:def 2; :: thesis: verum

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

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

reconsider u = u as Element of NAT by A18;

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

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

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

A22: 1 < u

proof

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

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

Seg k = { l where l is Nat : ( 1 <= l & l <= 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),sm)) = Seg k by FINSEQ_1:def 2;

Seg k = { l where l is Nat : ( 1 <= l & l <= 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),sm)) /. 1 in rng (SgmX ((BagOrder n),sm)) by A14, FUNCT_1:3;

then (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def 1

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

hence contradiction by A10, A14, A18, A22, PRE_POLY:def 2; :: thesis: verum

u in dom (SgmX ((BagOrder n),sm)) by A14, TARSKI:def 1;

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

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

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

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

then A26: (SgmX ((BagOrder n),sm)) /. 1 = b by A12, TARSKI:def 1;

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

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

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

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

.= ((m * (SgmX ((BagOrder n),sm))) /. 1) * (eval (b,x)) by A26, A1, A3, A27 ;

then y = <*((coefficient m) * (eval (b,x)))*> by A1, A27, A16, FINSEQ_1:40;

hence eval (m,x) = (coefficient m) * (eval (b,x)) by A2, RLVECT_1:44

.= (coefficient m) * (eval ((term m),x)) by A5, Def5 ;

:: thesis: verum

case A28:
m . b = 0. L
; :: thesis: eval (m,x) = (coefficient m) * (eval ((term m),x))

A29:
Support m = {}

then A30: (coefficient m) * (eval ((term m),x)) = 0. L ;

consider y being FinSequence of the carrier of L such that

A31: len y = len (SgmX ((BagOrder n),(Support m))) and

A32: eval (m,x) = Sum y and

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

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

BagOrder n linearly_orders Support m by POLYNOM2:18;

then rng (SgmX ((BagOrder n),(Support m))) = {} by A29, PRE_POLY:def 2;

then SgmX ((BagOrder n),(Support m)) = {} by RELAT_1:41;

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

hence eval (m,x) = (coefficient m) * (eval ((term m),x)) by A30, A32, RLVECT_1:43; :: thesis: verum

end;proof

then
( term m = EmptyBag n & m . (EmptyBag n) = 0. L )
by Def5, POLYNOM1:def 4;
assume
Support m <> {}
; :: thesis: contradiction

then reconsider sm = Support m as non empty Subset of (Bags n) ;

set c = the Element of sm;

m . the Element of sm <> 0. L by POLYNOM1:def 4;

hence contradiction by A4, A28; :: thesis: verum

end;then reconsider sm = Support m as non empty Subset of (Bags n) ;

set c = the Element of sm;

m . the Element of sm <> 0. L by POLYNOM1:def 4;

hence contradiction by A4, A28; :: thesis: verum

then A30: (coefficient m) * (eval ((term m),x)) = 0. L ;

consider y being FinSequence of the carrier of L such that

A31: len y = len (SgmX ((BagOrder n),(Support m))) and

A32: eval (m,x) = Sum y and

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

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

BagOrder n linearly_orders Support m by POLYNOM2:18;

then rng (SgmX ((BagOrder n),(Support m))) = {} by A29, PRE_POLY:def 2;

then SgmX ((BagOrder n),(Support m)) = {} by RELAT_1:41;

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

hence eval (m,x) = (coefficient m) * (eval ((term m),x)) by A30, A32, RLVECT_1:43; :: thesis: verum