let n be Ordinal; for L being non empty right_complementable distributive Abelian add-associative right_zeroed associative doubleLoopStr
for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
let L be non empty right_complementable distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for p, q, r being Series of n,L holds p *' (q + r) = (p *' q) + (p *' r)
let p, q, r be Series of n,L; p *' (q + r) = (p *' q) + (p *' r)
set cL = the carrier of L;
now for b being Element of Bags n holds (p *' (q + r)) . b = ((p *' q) + (p *' r)) . blet b be
Element of
Bags n;
(p *' (q + r)) . b = ((p *' q) + (p *' 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 . b1) * ((q + r) . b2) )
by Def10;
consider u being
FinSequence of the
carrier of
L such that A4:
(p *' 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 = (p . b1) * (r . b2) )
by Def10;
consider t being
FinSequence of the
carrier of
L such that A7:
(p *' q) . 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) * (q . b2) )
by Def10;
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, Th1;
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 . sb1) * ((q + 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 = (p . 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) * (q . 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 . sb2) + (r . sb2))
by A16, Th15
.=
((p . sb1) * (q . sb2)) + ((p . 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 *' q) + (p *' r)) . b
by A7, A4, Th15
;
verum end;
hence
p *' (q + r) = (p *' q) + (p *' r)
; verum