let n be Ordinal; :: thesis: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for m being Monomial of n,L
for b being bag of holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let p be Polynomial of n,L; :: thesis: for m being Monomial of n,L
for b being bag of holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let m be Monomial of n,L; :: thesis: for b being bag of holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let b2 be bag of ; :: thesis: (m *' p) . ((term m) + b2) = (m . (term m)) * (p . b2)
set q = m *' p;
set b = (term m) + b2;
consider s being FinSequence of the carrier of L such that
A1: ( (m *' p) . ((term m) + b2) = Sum s & len s = len (decomp ((term m) + b2)) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of st
( (decomp ((term m) + b2)) /. k = <*b1,b2*> & s /. k = (m . b1) * (p . b2) ) ) ) by POLYNOM1:def 26;
A2: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom (decomp ((term m) + b2)) by A1, FINSEQ_1:def 3 ;
consider k being Element of NAT such that
A3: ( k in dom (decomp ((term m) + b2)) & (decomp ((term m) + b2)) /. k = <*(term m),b2*> ) by POLYNOM1:73;
consider b1', b2' being bag of such that
A4: ( (decomp ((term m) + b2)) /. k = <*b1',b2'*> & s /. k = (m . b1') * (p . b2') ) by A1, A2, A3;
A5: term m = <*b1',b2'*> . 1 by A3, A4, FINSEQ_1:61
.= b1' by FINSEQ_1:61 ;
A6: b2 = <*(term m),b2*> . 2 by FINSEQ_1:61
.= b2' by A3, A4, FINSEQ_1:61 ;
for k' being Element of NAT st k' in dom s & k' <> k holds
s /. k' = 0. L

proof

let k' be Element of NAT ; :: thesis: ( k' in dom s & k' <> k implies s /. k' = 0. L )
assume A7: ( k' in dom s & k' <> k ) ; :: thesis: s /. k' = 0. L
then consider b1', b2' being bag of such that
A8: ( (decomp ((term m) + b2)) /. k' = <*b1',b2'*> & s /. k' = (m . b1') * (p . b2') ) by A1;
A9: b1' = (divisors ((term m) + b2)) /. k' by A2, A7, A8, POLYNOM1:74;
A10: ((term m) + b2) -' b1' = <*b1',(((term m) + b2) -' b1')*> . 2 by FINSEQ_1:61
.= <*b1',b2'*> . 2 by A2, A7, A8, A9, POLYNOM1:def 19
.= b2' by FINSEQ_1:61 ;

per cases ( ( b1' = term m & b2' = b2 ) or b1' <> term m or b2' <> b2 ) ;

suppose A11: ( b1' = term m & b2' = b2 ) ; :: thesis: s /. k' = 0. L

(decomp ((term m) + b2)) . k' = (decomp ((term m) + b2)) /. k' by A2, A7, PARTFUN1:def 8
.= (decomp ((term m) + b2)) . k by A3, A8, A11, PARTFUN1:def 8 ;
hence s /. k' = 0. L by A2, A3, A7, FUNCT_1:def 8; :: thesis: verum

end;

suppose b1' <> term m ; :: thesis: s /. k' = 0. L

then m . b1' = 0. L by Lm8;
hence s /. k' = 0. L by A8, VECTSP_1:39; :: thesis: verum

end;

suppose b2' <> b2 ; :: thesis: s /. k' = 0. L

then b1' <> term m by A10, POLYNOM1:52;
then m . b1' = 0. L by Lm8;
hence s /. k' = 0. L by A8, VECTSP_1:39; :: thesis: verum

end;

end;

end;

hence (m *' p) . ((term m) + b2) = (m . (term m)) * (p . b2) by A1, A2, A3, A4, A5, A6, POLYNOM2:5; :: thesis: verum