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