let r be Real; :: thesis: for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F)
let F be real-valued FinSequence; :: thesis: Sum (<*r*> ^ F) = r + (Sum F)
reconsider s = r as Element of REAL by XREAL_0:def 1;
thus Sum (<*r*> ^ F) = (Sum <*s*>) + (Sum F) by Th75
.= r + (Sum F) by FINSOP_1:11 ; :: thesis: verum