let n be Ordinal; for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let L be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; for p, q being Polynomial of n,L holds Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
let p, q be Polynomial of n,L; Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
A1:
now for b being bag of n st b in Support (p *' q) holds
ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )let b be
bag of
n;
( b in Support (p *' q) implies ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) )consider s being
FinSequence of
L such that A2:
(p *' q) . b = Sum s
and A3:
len s = len (decomp b)
and A4:
for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (p . b1) * (q . b2) )
by POLYNOM1:def 10;
A5:
dom s =
Seg (len (decomp b))
by A3, FINSEQ_1:def 3
.=
dom (decomp b)
by FINSEQ_1:def 3
;
assume A6:
b in Support (p *' q)
;
ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )now ( ( dom s = {} & contradiction ) or ( dom s <> {} & ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t ) ) )per cases
( dom s = {} or dom s <> {} )
;
case A7:
dom s <> {}
;
ex s, t being bag of n st
( s in Support p & t in Support q & b = s + t )set k = the
Element of
dom s;
the
Element of
dom s in dom s
by A7;
then reconsider k = the
Element of
dom s as
Element of
NAT ;
then consider k being
Element of
dom (decomp b),
b1,
b2 being
bag of
n such that A13:
(decomp b) /. k = <*b1,b2*>
and A14:
p . b1 <> 0. L
and A15:
q . b2 <> 0. L
;
k in dom (decomp b)
by A5, A7;
then reconsider k =
k as
Element of
NAT ;
consider b19,
b29 being
bag of
n such that A16:
(decomp b) /. k = <*b19,b29*>
and A17:
b = b19 + b29
by A5, A7, PRE_POLY:68;
A18:
b29 =
<*b1,b2*> . 2
by A13, A16, FINSEQ_1:44
.=
b2
by FINSEQ_1:44
;
b2 is
Element of
Bags n
by PRE_POLY:def 12;
then A19:
b2 in Support q
by A15, POLYNOM1:def 4;
b1 is
Element of
Bags n
by PRE_POLY:def 12;
then A20:
b1 in Support p
by A14, POLYNOM1:def 4;
b19 =
<*b1,b2*> . 1
by A13, A16, FINSEQ_1:44
.=
b1
by FINSEQ_1:44
;
hence
ex
s,
t being
bag of
n st
(
s in Support p &
t in Support q &
b = s + t )
by A20, A19, A17, A18;
verum end; hence
ex
s,
t being
bag of
n st
(
s in Support p &
t in Support q &
b = s + t )
;
verum end;
hence
Support (p *' q) c= { (s + t) where s, t is Element of Bags n : ( s in Support p & t in Support q ) }
; verum