let L be non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; for p being sequence of L holds p *' (1_. L) = p
let p be sequence of L; p *' (1_. L) = p
now for i being Element of NAT holds (p *' (1_. L)) . i = p . ilet i be
Element of
NAT ;
(p *' (1_. L)) . i = p . iconsider r being
FinSequence of the
carrier of
L such that A1:
len r = i + 1
and A2:
(p *' (1_. L)) . i = Sum r
and A3:
for
k being
Element of
NAT st
k in dom r holds
r . k = (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k))
by Def9;
a1:
r <> {}
by A1;
i + 1
in Seg (len r)
by A1, FINSEQ_1:4;
then A4:
i + 1
in dom r
by FINSEQ_1:def 3;
now for k being Element of NAT st k in dom (Del (r,(i + 1))) holds
(Del (r,(i + 1))) . k = 0. Llet k be
Element of
NAT ;
( k in dom (Del (r,(i + 1))) implies (Del (r,(i + 1))) . k = 0. L )assume
k in dom (Del (r,(i + 1)))
;
(Del (r,(i + 1))) . k = 0. Lthen A5:
k in Seg (len (Del (r,(i + 1))))
by FINSEQ_1:def 3;
then
k in Seg i
by A1, PRE_POLY:12;
then A6:
k <= i
by FINSEQ_1:1;
then A7:
k < i + 1
by NAT_1:13;
A8:
(i + 1) - k <> 0
by A6, NAT_1:13;
(i + 1) - k >= 0
by A7, XREAL_1:48;
then A9:
(i + 1) -' k <> 0
by A8, XREAL_0:def 2;
1
<= k
by A5, FINSEQ_1:1;
then
k in Seg (i + 1)
by A7, FINSEQ_1:1;
then A10:
k in dom r
by A1, FINSEQ_1:def 3;
thus (Del (r,(i + 1))) . k =
r . k
by A7, FINSEQ_3:110
.=
(p . (k -' 1)) * ((1_. L) . ((i + 1) -' k))
by A3, A10
.=
(p . (k -' 1)) * (0. L)
by A9, Th28
.=
0. L
;
verum end; then A11:
Sum (Del (r,(i + 1))) = 0. L
by Th1;
r =
(Del (r,(i + 1))) ^ <*(r . (i + 1))*>
by A1, a1, PRE_POLY:13
.=
(Del (r,(i + 1))) ^ <*(r /. (i + 1))*>
by A4, PARTFUN1:def 6
;
then A12:
Sum r =
(Sum (Del (r,(i + 1)))) + (Sum <*(r /. (i + 1))*>)
by RLVECT_1:41
.=
(Sum (Del (r,(i + 1)))) + (r /. (i + 1))
by RLVECT_1:44
;
r /. (i + 1) =
r . (i + 1)
by A4, PARTFUN1:def 6
.=
(p . ((i + 1) -' 1)) * ((1_. L) . ((i + 1) -' (i + 1)))
by A3, A4
.=
(p . i) * ((1_. L) . ((i + 1) -' (i + 1)))
by NAT_D:34
.=
(p . i) * ((1_. L) . 0)
by XREAL_1:232
.=
(p . i) * (1_ L)
by Th28
.=
p . i
;
hence
(p *' (1_. L)) . i = p . i
by A2, A12, A11, RLVECT_1:4;
verum end;
hence
p *' (1_. L) = p
; verum