let n be Ordinal; for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, p9 being Series of n,L
for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for p, p9 being Series of n,L
for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let p, p9 be Series of n,L; for a being Element of L holds a * (p *' p9) = p *' (a * p9)
let a be Element of L; a * (p *' p9) = p *' (a * p9)
set app = a * (p *' p9);
set pap = p *' (a * p9);
set pp = p *' p9;
A1:
now for u being object st u in dom (a * (p *' p9)) holds
(a * (p *' p9)) . u = (p *' (a * p9)) . ulet u be
object ;
( u in dom (a * (p *' p9)) implies (a * (p *' p9)) . u = (p *' (a * p9)) . u )assume
u in dom (a * (p *' p9))
;
(a * (p *' p9)) . u = (p *' (a * p9)) . uthen reconsider b =
u as
bag of
n ;
consider s being
FinSequence of the
carrier of
L such that A2:
(p *' (a * p9)) . 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) * ((a * p9) . b2) )
by POLYNOM1:def 10;
consider t being
FinSequence of the
carrier of
L such that A5:
(p *' p9) . b = Sum t
and A6:
len t = len (decomp b)
and A7:
for
k being
Element of
NAT st
k in dom t holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
t /. k = (p . b1) * (p9 . b2) )
by POLYNOM1:def 10;
A8:
dom t =
Seg (len s)
by A3, A6, FINSEQ_1:def 3
.=
dom s
by FINSEQ_1:def 3
;
now for i being object st i in dom t holds
s /. i = a * (t /. i)let i be
object ;
( i in dom t implies s /. i = a * (t /. i) )assume A9:
i in dom t
;
s /. i = a * (t /. i)then reconsider k =
i as
Element of
NAT ;
consider b1,
b2 being
bag of
n such that A10:
(decomp b) /. k = <*b1,b2*>
and A11:
t /. k = (p . b1) * (p9 . b2)
by A7, A9;
consider a1,
a2 being
bag of
n such that A12:
(decomp b) /. k = <*a1,a2*>
and A13:
s /. k = (p . a1) * ((a * p9) . a2)
by A4, A8, A9;
A14:
b2 =
<*a1,a2*> . 2
by A10, A12, FINSEQ_1:44
.=
a2
by FINSEQ_1:44
;
b1 =
<*a1,a2*> . 1
by A10, A12, FINSEQ_1:44
.=
a1
by FINSEQ_1:44
;
hence s /. i =
(p . b1) * (a * (p9 . b2))
by A13, A14, POLYNOM7:def 9
.=
a * (t /. i)
by A11, GROUP_1:def 3
;
verum end; then
s = a * t
by A8, POLYNOM1:def 1;
then (p *' (a * p9)) . b =
a * (Sum t)
by A2, POLYNOM1:12
.=
(a * (p *' p9)) . b
by A5, POLYNOM7:def 9
;
hence
(a * (p *' p9)) . u = (p *' (a * p9)) . u
;
verum end;
dom (a * (p *' p9)) =
Bags n
by FUNCT_2:def 1
.=
dom (p *' (a * p9))
by FUNCT_2:def 1
;
hence
a * (p *' p9) = p *' (a * p9)
by A1, FUNCT_1:2; verum