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