let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr ; for p being sequence of L holds (1_. L) *' p = p
let p be sequence of L; (1_. L) *' p = p
now for i being Element of NAT holds ((1_. L) *' p) . i = p . ilet i be
Element of
NAT ;
((1_. L) *' p) . i = p . iconsider r being
FinSequence of the
carrier of
L such that A1:
len r = i + 1
and A2:
((1_. L) *' p) . i = Sum r
and A3:
for
k being
Element of
NAT st
k in dom r holds
r . k = ((1_. L) . (k -' 1)) * (p . ((i + 1) -' k))
by Def9;
A4:
1
in dom r
by A1, CARD_1:27, FINSEQ_5:6;
now for k being Element of NAT st k in dom (Del (r,1)) holds
(Del (r,1)) . k = 0. Llet k be
Element of
NAT ;
( k in dom (Del (r,1)) implies (Del (r,1)) . k = 0. L )A5:
k + 1
>= 1
by NAT_1:11;
assume A6:
k in dom (Del (r,1))
;
(Del (r,1)) . k = 0. Lthen A7:
k <> 0
by FINSEQ_3:25;
len (Del (r,1)) = i
by A1, A4, FINSEQ_3:109;
then A8:
k <= i
by A6, FINSEQ_3:25;
then
k + 1
<= i + 1
by XREAL_1:6;
then A9:
k + 1
in dom r
by A1, A5, FINSEQ_3:25;
0 + 1
<= k
by A6, FINSEQ_3:25;
hence (Del (r,1)) . k =
r . (k + 1)
by A1, A4, A8, FINSEQ_3:111
.=
((1_. L) . ((k + 1) -' 1)) * (p . ((i + 1) -' (k + 1)))
by A3, A9
.=
((1_. L) . k) * (p . ((i + 1) -' (k + 1)))
by NAT_D:34
.=
(0. L) * (p . ((i + 1) -' (k + 1)))
by A7, Th28
.=
0. L
;
verum end; then A10:
Sum (Del (r,1)) = 0. L
by Th1;
r =
<*(r . 1)*> ^ (Del (r,1))
by A1, FINSEQ_5:86, CARD_1:27
.=
<*(r /. 1)*> ^ (Del (r,1))
by A4, PARTFUN1:def 6
;
then A11:
Sum r =
(Sum <*(r /. 1)*>) + (Sum (Del (r,1)))
by RLVECT_1:41
.=
(r /. 1) + (Sum (Del (r,1)))
by RLVECT_1:44
;
r /. 1 =
r . 1
by A4, PARTFUN1:def 6
.=
((1_. L) . (1 -' 1)) * (p . ((i + 1) -' 1))
by A3, A4
.=
((1_. L) . (1 -' 1)) * (p . i)
by NAT_D:34
.=
((1_. L) . 0) * (p . i)
by XREAL_1:232
.=
(1_ L) * (p . i)
by Th28
.=
p . i
;
hence
((1_. L) *' p) . i = p . i
by A2, A11, A10, RLVECT_1:4;
verum end;
hence
(1_. L) *' p = p
; verum