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
now :: thesis: for i being Element of NAT holds (p *' (1_. L)) . i = p . i
let 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 ;
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
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 ;
then A6: k <= i by FINSEQ_1:1;
then A7: k < i + 1 by NAT_1:13;
A8: (i + 1) - k <> 0 by ;
(i + 1) - k >= 0 by ;
then A9: (i + 1) -' k <> 0 by ;
1 <= k by ;
then k in Seg (i + 1) by ;
then A10: k in dom r by ;
thus (Del (r,(i + 1))) . k = r . k by
.= (p . (k -' 1)) * ((1_. L) . ((i + 1) -' k)) by
.= (p . (k -' 1)) * (0. L) by
.= 0. L ; :: thesis: verum
end;
then A11: Sum (Del (r,(i + 1))) = 0. L by Th1;
r = (Del (r,(i + 1))) ^ <*(r . (i + 1))*> by
.= (Del (r,(i + 1))) ^ <*(r /. (i + 1))*> by ;
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
.= (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 ; :: thesis: verum
end;
hence p *' (1_. L) = p ; :: thesis: verum