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 let 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 Def11;
i + 1
in Seg (len r)
by A1, FINSEQ_1:6;
then A4:
i + 1
in dom r
by FINSEQ_1:def 3;
now let 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:3;
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:50;
then A9:
(i + 1) -' k <> 0
by A8, XREAL_0:def 2;
1
<= k
by A5, FINSEQ_1:3;
then
k in Seg (i + 1)
by A7, FINSEQ_1:3;
then A10:
k in dom r
by A1, FINSEQ_1:def 3;
thus (Del r,(i + 1)) . k =
r . k
by A7, FINSEQ_3:119
.=
(p . (k -' 1)) * ((1_. L) . ((i + 1) -' k))
by A3, A10
.=
(p . (k -' 1)) * (0. L)
by A9, Th31
.=
0. L
by VECTSP_1:36
;
verum end; then A11:
Sum (Del r,(i + 1)) = 0. L
by Th1;
r =
(Del r,(i + 1)) ^ <*(r . (i + 1))*>
by A1, PRE_POLY:13
.=
(Del r,(i + 1)) ^ <*(r /. (i + 1))*>
by A4, PARTFUN1:def 8
;
then A12:
Sum r =
(Sum (Del r,(i + 1))) + (Sum <*(r /. (i + 1))*>)
by RLVECT_1:58
.=
(Sum (Del r,(i + 1))) + (r /. (i + 1))
by RLVECT_1:61
;
r /. (i + 1) =
r . (i + 1)
by A4, PARTFUN1:def 8
.=
(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:234
.=
(p . i) * (1_ L)
by Th31
.=
p . i
by VECTSP_1:def 13
;
hence
(p *' (1_. L)) . i = p . i
by A2, A12, A11, RLVECT_1:10;
verum end;
hence
p *' (1_. L) = p
by FUNCT_2:113; verum