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
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
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
for a being Element of L holds a * (b *' p) = (Monom a,b) *' p
let b be bag of ; :: 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 q' = (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 15;
A1: dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom ((Monom a,b) *' p) by FUNCT_2:def 1 ;

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 by POLYNOM1:def 14;
consider t being FinSequence of the carrier of L such that
A2: ( ((Monom a,b) *' p) . s = Sum t & len t = len (decomp s) & ( for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom a,b) . b1) * (p . b2) ) ) ) by POLYNOM1:def 26;
A3: term (Monom a,b) = b by POLYNOM7:10;
A4: dom t = Seg (len (decomp s)) by A2, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;

now

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

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

then consider s' being bag of such that
A6: b + s' = s by TERMORD:1;
A7: (a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 10
.= a * (p . (s -' b)) by A5, Def1 ;
consider i being Element of NAT such that
A8: ( i in dom (decomp s) & (decomp s) /. i = <*b,s'*> ) by A6, POLYNOM1:73;
A9: s -' b = s' by A6, POLYNOM1:52;
consider b1, b2 being bag of such that
A10: ( (decomp s) /. i = <*b1,b2*> & t /. i = ((Monom a,b) . b1) * (p . b2) ) by A2, A4, A8;
A11: b1 = <*b,s'*> . 1 by A8, A10, FINSEQ_1:61
.= b by FINSEQ_1:61 ;
A12: b2 = <*b,s'*> . 2 by A8, A10, FINSEQ_1:61
.= s' by FINSEQ_1:61 ;

now

let i' be Element of NAT ; :: thesis: ( i' in dom t & i' <> i implies t /. i' = 0. L )
assume A13: ( i' in dom t & i' <> i ) ; :: thesis: t /. i' = 0. L
then consider b1', b2' being bag of such that
A14: ( (decomp s) /. i' = <*b1',b2'*> & t /. i' = ((Monom a,b) . b1') * (p . b2') ) by A2;
consider h1, h2 being bag of such that
A15: ( (decomp s) /. i' = <*h1,h2*> & s = h1 + h2 ) by A4, A13, POLYNOM1:72;
A16: h1 = <*b1',b2'*> . 1 by A14, A15, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A17: s -' h1 = h2 by A15, POLYNOM1:52;

now

assume (Monom a,b) . b1' <> 0. L ; :: thesis: contradiction
then b1' = b by A3, POLYNOM7:def 6;
then (decomp s) . i' = (decomp s) /. i by A4, A8, A9, A13, A15, A16, A17, PARTFUN1:def 8
.= (decomp s) . i by A8, PARTFUN1:def 8 ;
hence contradiction by A4, A8, A13, FUNCT_1:def 8; :: thesis: verum

end;

hence t /. i' = 0. L by A14, BINOM:1; :: thesis: verum

end;

then Sum t = ((Monom a,b) . b) * (p . (s -' b)) by A4, A8, A9, A10, A11, A12, POLYNOM2:5
.= (coefficient (Monom a,b)) * (p . (s -' b)) by A3
.= a * (p . (s -' b)) by POLYNOM7:9 ;
hence (a * (b *' p)) . s = ((Monom a,b) *' p) . s by A2, A7; :: thesis: verum

end;

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

A19: (a * (b *' p)) . s = a * ((b *' p) . s) by POLYNOM7:def 10
.= a * (0. L) by A18, Def1
.= 0. L by BINOM:2 ;
consider t being FinSequence of the carrier of L such that
A20: ( ((Monom a,b) *' p) . s = Sum t & len t = len (decomp s) & ( for k being Element of NAT st k in dom t holds
ex b1, b2 being bag of st
( (decomp s) /. k = <*b1,b2*> & t /. k = ((Monom a,b) . b1) * (p . b2) ) ) ) by POLYNOM1:def 26;

now

let k be Nat; :: thesis: ( k in dom t implies t /. k = 0. L )
assume A21: k in dom t ; :: thesis: t /. k = 0. L
then consider b1', b2' being bag of such that
A22: ( (decomp s) /. k = <*b1',b2'*> & t /. k = ((Monom a,b) . b1') * (p . b2') ) by A20;
A23: dom t = Seg (len (decomp s)) by A20, FINSEQ_1:def 3
.= dom (decomp s) by FINSEQ_1:def 3 ;

now

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

case A24: b1' = term (Monom a,b) ; :: thesis: contradiction

consider h1, h2 being bag of such that
A25: ( (decomp s) /. k = <*h1,h2*> & s = h1 + h2 ) by A21, A23, POLYNOM1:72;
h1 = <*b1',b2'*> . 1 by A22, A25, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
hence contradiction by A3, A18, A24, A25, TERMORD:1; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence (a * (b *' p)) . u = ((Monom a,b) *' p) . u by A19, A20, MATRLIN:15; :: thesis: verum

end;

end;

end;

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

end;

hence a * (b *' p) = (Monom a,b) *' p by A1, FUNCT_1:9; :: thesis: verum

end;

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

A27: dom (a * (b *' p)) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;

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 u' = u as bag of by POLYNOM1:def 14;
(a * (b *' p)) . u' = (0. L) * ((b *' p) . u') by A26, POLYNOM7:def 10
.= 0. L by BINOM:1
.= (0_ n,L) . u' by POLYNOM1:81 ;
hence (a * (b *' p)) . u = (0_ n,L) . u ; :: thesis: verum

end;

then A28: a * (b *' p) = 0_ n,L by A27, FUNCT_1:9;
A29: dom (Monom a,b) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;

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 u' = u as Element of Bags n ;

now

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

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

then ( u' = EmptyBag n & coefficient (Monom a,b) = 0. L ) by A26, POLYNOM7:8;
then (Monom a,b) . u' = 0. L by A30;
hence (Monom a,b) . u = (0_ n,L) . u by POLYNOM1:81; :: thesis: verum

end;

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

then (Monom a,b) . u' = 0. L by Lm8
.= (0_ n,L) . u' 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;

then Monom a,b = 0_ n,L by A29, FUNCT_1:9;
hence a * (b *' p) = (Monom a,b) *' p by A28, Th5; :: thesis: verum

end;

end;