let r be real number ; :: thesis: for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r
let F be real-valued FinSequence; :: thesis: Sum (F ^ <*r*>) = (Sum F) + r
reconsider F1 = F as FinSequence of REAL by Lm4;
reconsider s = r as Element of REAL by XREAL_0:def 1;
thus Sum (F ^ <*r*>) = Sum (F1 ^ <*s*>)
.= addreal . (addreal $$ F1),s by FINSOP_1:5
.= (Sum F1) + r by BINOP_2:def 9
.= (Sum F) + r ; :: thesis: verum