let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr ; for p being sequence of L holds (1_. L) *' p = p
let p be sequence of L; (1_. L) *' p = p
now let 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 POLYNOM3:def 11;
A4:
1
in dom r
by A1, CARD_1:47, FINSEQ_5:6;
now let 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:27;
len (Del r,1) = i
by A1, A4, FINSEQ_3:118;
then A8:
k <= i
by A6, FINSEQ_3:27;
then
k + 1
<= i + 1
by XREAL_1:8;
then A9:
k + 1
in dom r
by A1, A5, FINSEQ_3:27;
0 + 1
<= k
by A6, FINSEQ_3:27;
hence (Del r,1) . k =
r . (k + 1)
by A1, A4, A8, FINSEQ_3:120
.=
((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, POLYNOM3:31
.=
0. L
by VECTSP_1:39
;
verum end; then A10:
Sum (Del r,1) = 0. L
by POLYNOM3:1;
r =
<*(r . 1)*> ^ (Del r,1)
by A1, Th4, CARD_1:47
.=
<*(r /. 1)*> ^ (Del r,1)
by A4, PARTFUN1:def 8
;
then A11:
Sum r =
(Sum <*(r /. 1)*>) + (Sum (Del r,1))
by RLVECT_1:58
.=
(r /. 1) + (Sum (Del r,1))
by RLVECT_1:61
;
r /. 1 =
r . 1
by A4, PARTFUN1:def 8
.=
((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:234
.=
(1_ L) * (p . i)
by POLYNOM3:31
.=
p . i
by VECTSP_1:def 19
;
hence
((1_. L) *' p) . i = p . i
by A2, A11, A10, RLVECT_1:10;
verum end;
hence
(1_. L) *' p = p
by FUNCT_2:113; verum