let L be non empty right_complementable add-associative right_zeroed right-distributive well-unital doubleLoopStr ; :: thesis: for p being sequence of L holds p *' (1_. L) = p

let p be sequence of L; :: thesis: p *' (1_. L) = p

let p be sequence of L; :: thesis: p *' (1_. L) = p

now :: thesis: for i being Element of NAT holds (p *' (1_. L)) . i = p . i

hence
p *' (1_. L) = p
; :: thesis: verumlet i be Element of NAT ; :: thesis: (p *' (1_. L)) . i = p . i

consider 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 Def9;

a1: r <> {} by A1;

i + 1 in Seg (len r) by A1, FINSEQ_1:4;

then A4: i + 1 in dom r by FINSEQ_1:def 3;

r = (Del (r,(i + 1))) ^ <*(r . (i + 1))*> by A1, a1, PRE_POLY:13

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

then A12: Sum r = (Sum (Del (r,(i + 1)))) + (Sum <*(r /. (i + 1))*>) by RLVECT_1:41

.= (Sum (Del (r,(i + 1)))) + (r /. (i + 1)) by RLVECT_1:44 ;

r /. (i + 1) = r . (i + 1) by A4, PARTFUN1:def 6

.= (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:232

.= (p . i) * (1_ L) by Th28

.= p . i ;

hence (p *' (1_. L)) . i = p . i by A2, A12, A11, RLVECT_1:4; :: thesis: verum

end;consider 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 Def9;

a1: r <> {} by A1;

i + 1 in Seg (len r) by A1, FINSEQ_1:4;

then A4: i + 1 in dom r by FINSEQ_1:def 3;

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

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

then A11:
Sum (Del (r,(i + 1))) = 0. L
by Th1;(Del (r,(i + 1))) . k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom (Del (r,(i + 1))) implies (Del (r,(i + 1))) . k = 0. L )

assume k in dom (Del (r,(i + 1))) ; :: thesis: (Del (r,(i + 1))) . k = 0. L

then 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:1;

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:48;

then A9: (i + 1) -' k <> 0 by A8, XREAL_0:def 2;

1 <= k by A5, FINSEQ_1:1;

then k in Seg (i + 1) by A7, FINSEQ_1:1;

then A10: k in dom r by A1, FINSEQ_1:def 3;

thus (Del (r,(i + 1))) . k = r . k by A7, FINSEQ_3:110

.= (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by A3, A10

.= (p . (k -' 1)) * (0. L) by A9, Th28

.= 0. L ; :: thesis: verum

end;assume k in dom (Del (r,(i + 1))) ; :: thesis: (Del (r,(i + 1))) . k = 0. L

then 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:1;

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:48;

then A9: (i + 1) -' k <> 0 by A8, XREAL_0:def 2;

1 <= k by A5, FINSEQ_1:1;

then k in Seg (i + 1) by A7, FINSEQ_1:1;

then A10: k in dom r by A1, FINSEQ_1:def 3;

thus (Del (r,(i + 1))) . k = r . k by A7, FINSEQ_3:110

.= (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by A3, A10

.= (p . (k -' 1)) * (0. L) by A9, Th28

.= 0. L ; :: thesis: verum

r = (Del (r,(i + 1))) ^ <*(r . (i + 1))*> by A1, a1, PRE_POLY:13

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

then A12: Sum r = (Sum (Del (r,(i + 1)))) + (Sum <*(r /. (i + 1))*>) by RLVECT_1:41

.= (Sum (Del (r,(i + 1)))) + (r /. (i + 1)) by RLVECT_1:44 ;

r /. (i + 1) = r . (i + 1) by A4, PARTFUN1:def 6

.= (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:232

.= (p . i) * (1_ L) by Th28

.= p . i ;

hence (p *' (1_. L)) . i = p . i by A2, A12, A11, RLVECT_1:4; :: thesis: verum