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