let K be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for a being Element of K
for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)
let a be Element of K; :: thesis: for p being FinSequence of the carrier of K holds Sum (<*a*> ^ p) = a + (Sum p)
let p be FinSequence of the carrier of K; :: thesis: Sum (<*a*> ^ p) = a + (Sum p)
thus Sum (<*a*> ^ p) = (Sum <*a*>) + (Sum p) by RLVECT_1:41
.= a + (Sum p) by RLVECT_1:44 ; :: thesis: verum