let n be Ordinal; :: thesis: for L being non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom a,b) *' p
let L be non trivial right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Series of n,L
for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom a,b) *' p
let p be Series of n,L; :: thesis: for b being bag of n
for a being Element of L holds a * (b *' p) = (Monom a,b) *' p
let b be bag of n; :: thesis: for a being Element of L holds a * (b *' p) = (Monom a,b) *' p
let a be Element of L; :: thesis: a * (b *' p) = (Monom a,b) *' p
set q = a * (b *' p);
set q9 = (Monom a,b) *' p;
set m = Monom a,b;

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

suppose a <> 0. L ; :: thesis: a * (b *' p) = (Monom a,b) *' p

then reconsider a = a as non zero Element of L by STRUCT_0:def 12;

A1: now

let u be set ; :: thesis: ( u in dom (a * (b *' p)) implies (a * (b *' p)) . u = ((Monom a,b) *' p) . u )
assume u in dom (a * (b *' p)) ; :: thesis: (a * (b *' p)) . u = ((Monom a,b) *' p) . u
then reconsider s = u as bag of n by PRE_POLY:def 12;
consider t being FinSequence of the carrier of L such that
A2: ((Monom a,b) *' p) . s = Sum t and
A3: len t = len (decomp s) and
A4: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom a,b) . b1) * (p . b2) ) by POLYNOM1:def 26;
A5: dom t = Seg (len (decomp s)) by A3, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;
A6: term (Monom a,b) = b by POLYNOM7:10;

now

per cases ( b divides s or not b divides s ) ;

case A7: b divides s ; :: thesis: (a * (b *' p)) . s = ((Monom a,b) *' p) . s

A8: (a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 10
.= a * (p . (s -' b)) by A7, Def1 ;
consider s9 being bag of n such that
A9: b + s9 = s by A7, TERMORD:1;
consider i being Element of NAT such that
A10: i in dom (decomp s) and
A11: (decomp s) /. i = <*b,s9*> by A9, PRE_POLY:69;
consider b1, b2 being bag of n such that
A12: (decomp s) /. i = <*b1,b2*> and
A13: t /. i = ((Monom a,b) . b1) * (p . b2) by A4, A5, A10;
A14: b2 = <*b,s9*> . 2 by A11, A12, FINSEQ_1:61
.= s9 by FINSEQ_1:61 ;
A15: s -' b = s9 by A9, PRE_POLY:48;

A16: now

let i9 be Element of NAT ; :: thesis: ( i9 in dom t & i9 <> i implies t /. i9 = 0. L )
assume that
A17: i9 in dom t and
A18: i9 <> i ; :: thesis: t /. i9 = 0. L
consider b19, b29 being bag of n such that
A19: (decomp s) /. i9 = <*b19,b29*> and
A20: t /. i9 = ((Monom a,b) . b19) * (p . b29) by A4, A17;
consider h1, h2 being bag of n such that
A21: (decomp s) /. i9 = <*h1,h2*> and
A22: s = h1 + h2 by A5, A17, PRE_POLY:68;
A23: s -' h1 = h2 by A22, PRE_POLY:48;
A24: h1 = <*b19,b29*> . 1 by A19, A21, FINSEQ_1:61
.= b19 by FINSEQ_1:61 ;

now

assume (Monom a,b) . b19 <> 0. L ; :: thesis: contradiction
then b19 = b by A6, POLYNOM7:def 6;
then (decomp s) . i9 = (decomp s) /. i by A5, A11, A15, A17, A21, A24, A23, PARTFUN1:def 8
.= (decomp s) . i by A10, PARTFUN1:def 8 ;
hence contradiction by A5, A10, A17, A18, FUNCT_1:def 8; :: thesis: verum

end;

hence t /. i9 = 0. L by A20, BINOM:1; :: thesis: verum

end;

b1 = <*b,s9*> . 1 by A11, A12, FINSEQ_1:61
.= b by FINSEQ_1:61 ;
then Sum t = ((Monom a,b) . b) * (p . (s -' b)) by A5, A10, A15, A13, A14, A16, POLYNOM2:5
.= (coefficient (Monom a,b)) * (p . (s -' b)) by A6
.= a * (p . (s -' b)) by POLYNOM7:9 ;
hence (a * (b *' p)) . s = ((Monom a,b) *' p) . s by A2, A8; :: thesis: verum

end;

case A25: not b divides s ; :: thesis: (a * (b *' p)) . u = ((Monom a,b) *' p) . u

consider t being FinSequence of the carrier of L such that
A26: ((Monom a,b) *' p) . s = Sum t and
A27: len t = len (decomp s) and
A28: for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of n st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom a,b) . b1) * (p . b2) ) by POLYNOM1:def 26;

A29: now

let k be Nat; :: thesis: ( k in dom t implies t /. k = 0. L )
assume A30: k in dom t ; :: thesis: t /. k = 0. L
then consider b19, b29 being bag of n such that
A31: (decomp s) /. k = <*b19,b29*> and
A32: t /. k = ((Monom a,b) . b19) * (p . b29) by A28;
A33: dom t = Seg (len (decomp s)) by A27, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;

now

per cases ( b19 = term (Monom a,b) or b19 <> term (Monom a,b) ) ;

case A34: b19 = term (Monom a,b) ; :: thesis: contradiction

consider h1, h2 being bag of n such that
A35: (decomp s) /. k = <*h1,h2*> and
A36: s = h1 + h2 by A30, A33, PRE_POLY:68;
h1 = <*b19,b29*> . 1 by A31, A35, FINSEQ_1:61
.= b19 by FINSEQ_1:61 ;
hence contradiction by A6, A25, A34, A36, TERMORD:1; :: thesis: verum

end;

case b19 <> term (Monom a,b) ; :: thesis: (Monom a,b) . b19 = 0. L

hence (Monom a,b) . b19 = 0. L by Lm8; :: thesis: verum

end;

end;

end;

hence t /. k = 0. L by A32, BINOM:1; :: thesis: verum

end;

(a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 10
.= a * (0. L) by A25, Def1
.= 0. L by BINOM:2 ;
hence (a * (b *' p)) . u = ((Monom a,b) *' p) . u by A26, A29, MATRLIN:15; :: thesis: verum

end;

end;

end;

hence (a * (b *' p)) . u = ((Monom a,b) *' p) . u ; :: thesis: verum

end;

dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom ((Monom a,b) *' p) by FUNCT_2:def 1 ;
hence a * (b *' p) = (Monom a,b) *' p by A1, FUNCT_1:9; :: thesis: verum

end;

suppose A37: a = 0. L ; :: thesis: a * (b *' p) = (Monom a,b) *' p

A38: now

let u be set ; :: thesis: ( u in dom (Monom a,b) implies (Monom a,b) . u = (0_ n,L) . u )
assume u in dom (Monom a,b) ; :: thesis: (Monom a,b) . u = (0_ n,L) . u
then reconsider u9 = u as Element of Bags n ;

now

per cases ( u9 = term (Monom a,b) or u9 <> term (Monom a,b) ) ;

case A39: u9 = term (Monom a,b) ; :: thesis: (Monom a,b) . u = (0_ n,L) . u

coefficient (Monom a,b) = 0. L by A37, POLYNOM7:8;
hence (Monom a,b) . u = (0_ n,L) . u by A39, POLYNOM1:81; :: thesis: verum

end;

case u9 <> term (Monom a,b) ; :: thesis: (Monom a,b) . u = (0_ n,L) . u

then (Monom a,b) . u9 = 0. L by Lm8
.= (0_ n,L) . u9 by POLYNOM1:81 ;
hence (Monom a,b) . u = (0_ n,L) . u ; :: thesis: verum

end;

end;

end;

hence (Monom a,b) . u = (0_ n,L) . u ; :: thesis: verum

end;

dom (Monom a,b) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;
then A40: Monom a,b = 0_ n,L by A38, FUNCT_1:9;

A41: now

let u be set ; :: thesis: ( u in dom (a * (b *' p)) implies (a * (b *' p)) . u = (0_ n,L) . u )
assume u in dom (a * (b *' p)) ; :: thesis: (a * (b *' p)) . u = (0_ n,L) . u
then reconsider u9 = u as bag of n by PRE_POLY:def 12;
(a * (b *' p)) . u9 = (0. L) * ((b *' p) . u9) by A37, POLYNOM7:def 10
.= 0. L by BINOM:1
.= (0_ n,L) . u9 by POLYNOM1:81 ;
hence (a * (b *' p)) . u = (0_ n,L) . u ; :: thesis: verum

end;

dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;
then a * (b *' p) = 0_ n,L by A41, FUNCT_1:9;
hence a * (b *' p) = (Monom a,b) *' p by A40, Th5; :: thesis: verum

end;

end;