let n be Ordinal; for L being non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr
for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
let L be non empty right_complementable Abelian add-associative right_zeroed associative distributive doubleLoopStr ; for p, q, r being Series of n,L holds (p + q) *' r = (p *' r) + (q *' r)
let p, q, r be Series of n,L; (p + q) *' r = (p *' r) + (q *' r)
set cL = the carrier of L;
now for b being Element of Bags n holds ((p + q) *' r) . b = ((p *' r) + (q *' r)) . blet b be
Element of
Bags n;
((p + q) *' r) . b = ((p *' r) + (q *' r)) . bconsider s being
FinSequence of the
carrier of
L such that A1:
((p + q) *' r) . b = Sum s
and A2:
len s = len (decomp b)
and A3:
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 + q) . b1) * (r . b2) )
by POLYNOM1:def 10;
consider u being
FinSequence of the
carrier of
L such that A4:
(q *' r) . b = Sum u
and A5:
len u = len (decomp b)
and A6:
for
k being
Element of
NAT st
k in dom u holds
ex
b1,
b2 being
bag of
n st
(
(decomp b) /. k = <*b1,b2*> &
u /. k = (q . b1) * (r . b2) )
by POLYNOM1:def 10;
consider t being
FinSequence of the
carrier of
L such that A7:
(p *' r) . b = Sum t
and A8:
len t = len (decomp b)
and A9:
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) * (r . b2) )
by POLYNOM1:def 10;
reconsider t =
t,
u =
u as
Element of
(len s) -tuples_on the
carrier of
L by A2, A8, A5, FINSEQ_2:92;
A10:
dom u = dom s
by A2, A5, FINSEQ_3:29;
A11:
dom t = dom s
by A2, A8, FINSEQ_3:29;
then A12:
dom (t + u) = dom s
by A10, POLYNOM1:1;
A13:
now for i being Nat st i in dom s holds
s . i = (t + u) . ilet i be
Nat;
( i in dom s implies s . i = (t + u) . i )assume A14:
i in dom s
;
s . i = (t + u) . ithen consider sb1,
sb2 being
bag of
n such that A15:
(decomp b) /. i = <*sb1,sb2*>
and A16:
s /. i = ((p + q) . sb1) * (r . sb2)
by A3;
A17:
(
t /. i = t . i &
u /. i = u . i )
by A11, A10, A14, PARTFUN1:def 6;
consider ub1,
ub2 being
bag of
n such that A18:
(decomp b) /. i = <*ub1,ub2*>
and A19:
u /. i = (q . ub1) * (r . ub2)
by A6, A10, A14;
A20:
(
sb1 = ub1 &
sb2 = ub2 )
by A15, A18, FINSEQ_1:77;
consider tb1,
tb2 being
bag of
n such that A21:
(decomp b) /. i = <*tb1,tb2*>
and A22:
t /. i = (p . tb1) * (r . tb2)
by A9, A11, A14;
A23:
(
sb1 = tb1 &
sb2 = tb2 )
by A15, A21, FINSEQ_1:77;
s /. i = s . i
by A14, PARTFUN1:def 6;
hence s . i =
((p . sb1) + (q . sb1)) * (r . sb2)
by A16, POLYNOM1:15
.=
((p . sb1) * (r . sb2)) + ((q . sb1) * (r . sb2))
by VECTSP_1:def 7
.=
(t + u) . i
by A12, A14, A22, A19, A23, A20, A17, FVSUM_1:17
;
verum end;
len (t + u) = len s
by A12, FINSEQ_3:29;
then
s = t + u
by A13, FINSEQ_2:9;
hence ((p + q) *' r) . b =
(Sum t) + (Sum u)
by A1, FVSUM_1:76
.=
((p *' r) + (q *' r)) . b
by A7, A4, POLYNOM1:15
;
verum end;
hence
(p + q) *' r = (p *' r) + (q *' r)
by FUNCT_2:63; verum