let n be Ordinal; :: thesis: for L being non empty right_complementable associative distributive Abelian add-associative right_zeroed 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 associative distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: p *' (q + r) = (p *' q) + (p *' r)
set cL = the carrier of L;
now let b be
Element of
Bags n;
:: thesis: (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 st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (p . b1) * ((q + r) . b2) )
by Def26;
consider t being
FinSequence of the
carrier of
L such that A4:
(p *' q) . b = Sum t
and A5:
len t = len (decomp b)
and A6:
for
k being
Element of
NAT st
k in dom t holds
ex
b1,
b2 being
bag of st
(
(decomp b) /. k = <*b1,b2*> &
t /. k = (p . b1) * (q . b2) )
by Def26;
consider u being
FinSequence of the
carrier of
L such that A7:
(p *' r) . b = Sum u
and A8:
len u = len (decomp b)
and A9:
for
k being
Element of
NAT st
k in dom u holds
ex
b1,
b2 being
bag of st
(
(decomp b) /. k = <*b1,b2*> &
u /. k = (p . b1) * (r . b2) )
by Def26;
reconsider S =
s,
t =
t,
u =
u as
Element of
(len s) -tuples_on the
carrier of
L by A2, A5, A8, FINSEQ_2:110;
A10:
(
dom t = dom s &
dom u = dom s )
by A2, A5, A8, FINSEQ_3:31;
then A11:
dom (t + u) = dom s
by Th5;
then A12:
len (t + u) = len s
by FINSEQ_3:31;
X:
dom s = Seg (len s)
by FINSEQ_1:def 3;
now let i be
Nat;
:: thesis: ( i in dom s implies s . i = (t + u) . i )assume
i in dom s
;
:: thesis: s . i = (t + u) . ithen
( 1
<= i &
i <= len s )
by X, FINSEQ_1:3;
then A13:
i in dom s
by FINSEQ_3:27;
then consider sb1,
sb2 being
bag of
such that A14:
(
(decomp b) /. i = <*sb1,sb2*> &
s /. i = (p . sb1) * ((q + r) . sb2) )
by A3;
consider tb1,
tb2 being
bag of
such that A15:
(
(decomp b) /. i = <*tb1,tb2*> &
t /. i = (p . tb1) * (q . tb2) )
by A6, A10, A13;
consider ub1,
ub2 being
bag of
such that A16:
(
(decomp b) /. i = <*ub1,ub2*> &
u /. i = (p . ub1) * (r . ub2) )
by A9, A10, A13;
A17:
(
sb1 = tb1 &
sb1 = ub1 &
sb2 = tb2 &
sb2 = ub2 )
by A14, A15, A16, GROUP_7:2;
A18:
(
s /. i = s . i &
t /. i = t . i &
u /. i = u . i )
by A10, A13, PARTFUN1:def 8;
hence s . i =
(p . sb1) * ((q . sb2) + (r . sb2))
by A14, Def21
.=
((p . sb1) * (q . sb2)) + ((p . sb1) * (r . sb2))
by VECTSP_1:def 18
.=
(t + u) . i
by A11, A13, A15, A16, A17, A18, FVSUM_1:21
;
:: thesis: verum end; then
s = t + u
by A12, FINSEQ_2:10;
hence (p *' (q + r)) . b =
(Sum t) + (Sum u)
by A1, FVSUM_1:95
.=
((p *' q) + (p *' r)) . b
by A4, A7, Def21
;
:: thesis: verum end;
hence
p *' (q + r) = (p *' q) + (p *' r)
by FUNCT_2:113; :: thesis: verum