let L be non empty right_complementable add-associative right_zeroed left-distributive well-unital 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 :: thesis: for i being Element of NAT holds ((1_. L) *' p) . i = p . i
let i be Element of NAT ; :: thesis: ((1_. L) *' p) . i = p . i
consider 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 ;
now :: thesis: for k being Element of NAT st k in dom (Del (r,1)) holds
(Del (r,1)) . k = 0. L
let k be Element of NAT ; :: thesis: ( 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)) ; :: thesis: (Del (r,1)) . k = 0. L
then A7: k <> 0 by FINSEQ_3:25;
len (Del (r,1)) = i by ;
then A8: k <= i by ;
then k + 1 <= i + 1 by XREAL_1:6;
then A9: k + 1 in dom r by ;
0 + 1 <= k by ;
hence (Del (r,1)) . k = r . (k + 1) by
.= ((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
.= 0. L ;
:: thesis: verum
end;
then A10: Sum (Del (r,1)) = 0. L by Th1;
r = <*(r . 1)*> ^ (Del (r,1)) by
.= <*(r /. 1)*> ^ (Del (r,1)) by ;
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
.= ((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 ; :: thesis: verum
end;
hence (1_. L) *' p = p ; :: thesis: verum