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

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

hence
(1_. L) *' p = p
; :: thesis: verumlet 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 A1, CARD_1:27, FINSEQ_5:6;

r = <*(r . 1)*> ^ (Del (r,1)) by A1, FINSEQ_5:86, CARD_1:27

.= <*(r /. 1)*> ^ (Del (r,1)) by A4, PARTFUN1:def 6 ;

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 A4, PARTFUN1:def 6

.= ((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 A2, A11, A10, RLVECT_1:4; :: thesis: verum

end;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 A1, CARD_1:27, FINSEQ_5:6;

now :: thesis: for k being Element of NAT st k in dom (Del (r,1)) holds

(Del (r,1)) . k = 0. L

then A10:
Sum (Del (r,1)) = 0. L
by Th1;(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 A1, A4, FINSEQ_3:109;

then A8: k <= i by A6, FINSEQ_3:25;

then k + 1 <= i + 1 by XREAL_1:6;

then A9: k + 1 in dom r by A1, A5, FINSEQ_3:25;

0 + 1 <= k by A6, FINSEQ_3:25;

hence (Del (r,1)) . k = r . (k + 1) by A1, A4, A8, FINSEQ_3:111

.= ((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, Th28

.= 0. L ;

:: thesis: verum

end;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 A1, A4, FINSEQ_3:109;

then A8: k <= i by A6, FINSEQ_3:25;

then k + 1 <= i + 1 by XREAL_1:6;

then A9: k + 1 in dom r by A1, A5, FINSEQ_3:25;

0 + 1 <= k by A6, FINSEQ_3:25;

hence (Del (r,1)) . k = r . (k + 1) by A1, A4, A8, FINSEQ_3:111

.= ((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, Th28

.= 0. L ;

:: thesis: verum

r = <*(r . 1)*> ^ (Del (r,1)) by A1, FINSEQ_5:86, CARD_1:27

.= <*(r /. 1)*> ^ (Del (r,1)) by A4, PARTFUN1:def 6 ;

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 A4, PARTFUN1:def 6

.= ((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 A2, A11, A10, RLVECT_1:4; :: thesis: verum