let N be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of the carrier of N
for k being Nat st k in dom p holds
Sum p = (Sum (Del (p,k,k))) + (p /. k)
let p be FinSequence of the carrier of N; :: thesis: for k being Nat st k in dom p holds
Sum p = (Sum (Del (p,k,k))) + (p /. k)
let k be Nat; :: thesis: ( k in dom p implies Sum p = (Sum (Del (p,k,k))) + (p /. k) )
set a = p | (k -' 1);
set b = p /^ k;
set c = <*(p /. k)*>;
assume A1: k in dom p ; :: thesis: Sum p = (Sum (Del (p,k,k))) + (p /. k)
then ( 1 <= k & k <= len p ) by FINSEQ_3:25;
then p = ((p | (k -' 1)) ^ <*(p . k)*>) ^ (p /^ k) by FINSEQ_5:84
.= ((p | (k -' 1)) ^ <*(p /. k)*>) ^ (p /^ k) by A1, PARTFUN1:def 6 ;
then Sum p = (Sum ((p | (k -' 1)) ^ <*(p /. k)*>)) + (Sum (p /^ k)) by RLVECT_1:41
.= ((Sum (p | (k -' 1))) + (Sum <*(p /. k)*>)) + (Sum (p /^ k)) by RLVECT_1:41
.= ((Sum (p | (k -' 1))) + (Sum (p /^ k))) + (Sum <*(p /. k)*>) by RLVECT_1:def 3
.= (Sum (Del (p,k,k))) + (Sum <*(p /. k)*>) by RLVECT_1:41 ;
hence Sum p = (Sum (Del (p,k,k))) + (p /. k) by RLVECT_1:44; :: thesis: verum