let n be Ordinal; 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 ; 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; 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; for b being bag of n holds (m *' p) . ((term m) + b) = (m . (term m)) * (p . b)
let b2 be bag of n; (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
by FINSEQ_1:44
.=
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 ;
( k9 in dom s & k9 <> k implies s /. k9 = 0. L )
assume that A11:
k9 in dom s
and A12:
k9 <> k
;
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
by FINSEQ_1:44
.=
<*b19,b29*> . 2
by A6, A11, A13, A15, PRE_POLY:def 17
.=
b29
by FINSEQ_1:44
;
per cases
( ( b19 = term m & b29 = b2 ) or b19 <> term m or b29 <> b2 )
;
suppose A17:
(
b19 = term m &
b29 = b2 )
;
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;
verum end; end;
end;
term m =
<*b19,b29*> . 1
by A5, A7, FINSEQ_1:44
.=
b19
by FINSEQ_1:44
;
hence
(m *' p) . ((term m) + b2) = (m . (term m)) * (p . b2)
by A1, A6, A4, A8, A9, A10, POLYNOM2:3; verum