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 (p ^ <*a*>) = (Sum p) + a
let a be Element of K; :: thesis: for p being FinSequence of the carrier of K holds Sum (p ^ <*a*>) = (Sum p) + a
let p be FinSequence of the carrier of K; :: thesis: Sum (p ^ <*a*>) = (Sum p) + a
thus Sum (p ^ <*a*>) = (Sum p) + (Sum <*a*>) by RLVECT_1:41
.= (Sum p) + a by RLVECT_1:44 ; :: thesis: verum