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 26;
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 b1', b2' being bag of n such that
A7:
(decomp ((term m) + b2)) /. k = <*b1',b2'*>
and
A8:
s /. k = (m . b1') * (p . b2')
by A3, A4;
A9: b2 =
<*(term m),b2*> . 2
by FINSEQ_1:61
.=
b2'
by A5, A7, FINSEQ_1:61
;
A10:
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 ;
( k' in dom s & k' <> k implies s /. k' = 0. L )
assume that A11:
k' in dom s
and A12:
k' <> k
;
s /. k' = 0. L
consider b1',
b2' being
bag of
n such that A13:
(decomp ((term m) + b2)) /. k' = <*b1',b2'*>
and A14:
s /. k' = (m . b1') * (p . b2')
by A3, A11;
A15:
b1' = (divisors ((term m) + b2)) /. k'
by A6, A11, A13, PRE_POLY:70;
A16:
((term m) + b2) -' b1' =
<*b1',(((term m) + b2) -' b1')*> . 2
by FINSEQ_1:61
.=
<*b1',b2'*> . 2
by A6, A11, A13, A15, PRE_POLY:def 17
.=
b2'
by FINSEQ_1:61
;
per cases
( ( b1' = term m & b2' = b2 ) or b1' <> term m or b2' <> b2 )
;
suppose A17:
(
b1' = term m &
b2' = b2 )
;
s /. k' = 0. L(decomp ((term m) + b2)) . k' =
(decomp ((term m) + b2)) /. k'
by A6, A11, PARTFUN1:def 8
.=
(decomp ((term m) + b2)) . k
by A4, A5, A13, A17, PARTFUN1:def 8
;
hence
s /. k' = 0. L
by A6, A4, A11, A12, FUNCT_1:def 8;
verum end;
end;
term m =
<*b1',b2'*> . 1
by A5, A7, FINSEQ_1:61
.=
b1'
by FINSEQ_1:61
;
hence
(m *' p) . ((term m) + b2) = (m . (term m)) * (p . b2)
by A1, A6, A4, A8, A9, A10, POLYNOM2:5; verum