let n be Ordinal; for L being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for p being Series of n,L
for a being Element of L holds a * p = (a | n,L) *' p
let L be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; for p being Series of n,L
for a being Element of L holds a * p = (a | n,L) *' p
let p be Series of n,L; for a being Element of L holds a * p = (a | n,L) *' p
let a be Element of L; a * p = (a | n,L) *' p
A1:
for x being set st x in Bags n holds
(a * p) . x = ((a | n,L) *' p) . x
proof
set O =
a | n,
L;
set cL = the
carrier of
L;
let x be
set ;
( x in Bags n implies (a * p) . x = ((a | n,L) *' p) . x )
assume
x in Bags n
;
(a * p) . x = ((a | n,L) *' p) . x
then reconsider b =
x as
bag of
n ;
A2:
for
b being
Element of
Bags n holds
((a | n,L) *' p) . b = a * (p . b)
proof
let b be
Element of
Bags n;
((a | n,L) *' p) . b = a * (p . b)
consider s being
FinSequence of the
carrier of
L such that A3:
((a | n,L) *' p) . b = Sum s
and A4:
len s = len (decomp b)
and A5:
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 = ((a | n,L) . b1) * (p . b2) )
by POLYNOM1:def 26;
not
s is
empty
by A4;
then consider s1 being
Element of the
carrier of
L,
t being
FinSequence of the
carrier of
L such that A6:
s1 = s . 1
and A7:
s = <*s1*> ^ t
by FINSEQ_3:111;
A8:
Sum s = (Sum <*s1*>) + (Sum t)
by A7, RLVECT_1:58;
A9:
now per cases
( t = <*> the carrier of L or t <> <*> the carrier of L )
;
suppose A10:
t <> <*> the
carrier of
L
;
Sum t = 0. Lnow let k be
Nat;
( k in dom t implies t /. b1 = 0. L )A11:
len s =
(len t) + (len <*s1*>)
by A7, FINSEQ_1:35
.=
(len t) + 1
by FINSEQ_1:56
;
assume A12:
k in dom t
;
t /. b1 = 0. Lthen A13:
t /. k =
t . k
by PARTFUN1:def 8
.=
s . (k + 1)
by A7, A12, FINSEQ_3:112
;
1
<= k
by A12, FINSEQ_3:27;
then A14:
1
< k + 1
by NAT_1:13;
k <= len t
by A12, FINSEQ_3:27;
then A15:
k + 1
<= len s
by A11, XREAL_1:8;
then A16:
k + 1
in dom (decomp b)
by A4, A14, FINSEQ_3:27;
A17:
dom s = dom (decomp b)
by A4, FINSEQ_3:31;
then A18:
s /. (k + 1) = s . (k + 1)
by A16, PARTFUN1:def 8;
per cases
( k + 1 < len s or k + 1 = len s )
by A15, XXREAL_0:1;
suppose A19:
k + 1
< len s
;
t /. b1 = 0. Lreconsider k1 =
k as
Element of
NAT by ORDINAL1:def 13;
consider b1,
b2 being
bag of
n such that A20:
(decomp b) /. (k1 + 1) = <*b1,b2*>
and A21:
s /. (k1 + 1) = ((a | n,L) . b1) * (p . b2)
by A5, A17, A16;
b1 <> EmptyBag n
by A4, A14, A19, A20, PRE_POLY:72;
hence t /. k =
(0. L) * (p . b2)
by A13, A18, A21, Th18
.=
0. L
by VECTSP_1:39
;
verum end; suppose A22:
k + 1
= len s
;
t /. b1 = 0. Lconsider b1,
b2 being
bag of
n such that A24:
(decomp b) /. (k + 1) = <*b1,b2*>
and A25:
s /. (k + 1) = ((a | n,L) . b1) * (p . b2)
by A5, A17, A16;
(decomp b) /. (len s) = <*b,(EmptyBag n)*>
by A4, PRE_POLY:71;
then
(
b2 = EmptyBag n &
b1 = b )
by A22, A24, FINSEQ_1:98;
then s . (k + 1) =
(0. L) * (p . (EmptyBag n))
by A18, A25, A23, Th18
.=
0. L
by VECTSP_1:39
;
hence
t /. k = 0. L
by A13;
verum end; end; hence
Sum t = 0. L
by MATRLIN:15;
verum
A26:
not
s is
empty
by A4;
then consider b1,
b2 being
bag of
n such that A27:
(decomp b) /. 1
= <*b1,b2*>
and A28:
s /. 1
= ((a | n,L) . b1) * (p . b2)
by A5, FINSEQ_5:6;
1
in dom s
by A26, FINSEQ_5:6;
then A29:
s /. 1
= s . 1
by PARTFUN1:def 8;
(decomp b) /. 1
= <*(EmptyBag n),b*>
by PRE_POLY:71;
then A30:
(
b2 = b &
b1 = EmptyBag n )
by A27, FINSEQ_1:98;
Sum <*s1*> =
s1
by RLVECT_1:61
.=
a * (p . b)
by A6, A28, A30, A29, Th18
;
hence
((a | n,L) *' p) . b = a * (p . b)
by A3, A8, A9, RLVECT_1:10;
verum
end;
b is
Element of
Bags n
by PRE_POLY:def 12;
then ((a | n,L) *' p) . b =
a * (p . b)
by A2
.=
(a * p) . b
by Def10
;
hence
(a * p) . x = ((a | n,L) *' p) . x
;
verum
end;
( Bags n = dom (a * p) & Bags n = dom ((a | n,L) *' p) )
by FUNCT_2:def 1;
hence
a * p = (a | n,L) *' p
by A1, FUNCT_1:9; verum