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 n 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 n 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 n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let m be Monomial of n,L; :: thesis: for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let b2 be bag of n; :: 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 and
A2: len s = len (decomp ((term m) + b2)) and
A3: for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp ((term m) + b2)) /. k = <*b1,b2*> & s /. k = (m . b1) * (p . b2) ) by POLYNOM1:def 10;
consider k being Element of NAT such that
A4: k in dom (decomp ((term m) + b2)) and
A5: (decomp ((term m) + b2)) /. k = <*(term m),b2*> by PRE_POLY:69;
A6: dom s = Seg (len s) by FINSEQ_1:def 3
.= dom (decomp ((term m) + b2)) by A2, FINSEQ_1:def 3 ;
then consider b19, b29 being bag of n such that
A7: (decomp ((term m) + b2)) /. k = <*b19,b29*> and
A8: s /. k = (m . b19) * (p . b29) by A3, A4;
A9: b2 = <*(term m),b2*> . 2
.= b29 by A5, A7, FINSEQ_1:44 ;
A10: for k9 being Element of NAT st k9 in dom s & k9 <> k holds
s /. k9 = 0. L

proof

let k9 be Element of NAT ; :: thesis: ( k9 in dom s & k9 <> k implies s /. k9 = 0. L )
assume that
A11: k9 in dom s and
A12: k9 <> k ; :: thesis: s /. k9 = 0. L
consider b19, b29 being bag of n such that
A13: (decomp ((term m) + b2)) /. k9 = <*b19,b29*> and
A14: s /. k9 = (m . b19) * (p . b29) by A3, A11;
A15: b19 = (divisors ((term m) + b2)) /. k9 by A6, A11, A13, PRE_POLY:70;
A16: ((term m) + b2) -' b19 = <*b19,(((term m) + b2) -' b19)*> . 2
.= <*b19,b29*> . 2 by A6, A11, A13, A15, PRE_POLY:def 17
.= b29 ;

per cases ( ( b19 = term m & b29 = b2 ) or b19 <> term m or b29 <> b2 ) ;

suppose A17: ( b19 = term m & b29 = b2 ) ; :: thesis: s /. k9 = 0. L

(decomp ((term m) + b2)) . k9 = (decomp ((term m) + b2)) /. k9 by A6, A11, PARTFUN1:def 6
.= (decomp ((term m) + b2)) . k by A4, A5, A13, A17, PARTFUN1:def 6 ;
hence s /. k9 = 0. L by A6, A4, A11, A12, FUNCT_1:def 4; :: thesis: verum

end;

suppose b19 <> term m ; :: thesis: s /. k9 = 0. L

then m . b19 = 0. L by Lm8;
hence s /. k9 = 0. L by A14; :: thesis: verum

end;

suppose b29 <> b2 ; :: thesis: s /. k9 = 0. L

then b19 <> term m by A16, PRE_POLY:48;
then m . b19 = 0. L by Lm8;
hence s /. k9 = 0. L by A14; :: thesis: verum

end;

end;

end;

term m = <*b19,b29*> . 1 by A5, A7
.= b19 ;
hence (m *' p) . ((term m) + b2) = (m . (term m)) * (p . b2) by A1, A6, A4, A8, A9, A10, POLYNOM2:3; :: thesis: verum