let r be Real; :: 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 s = r as Element of REAL by XREAL_0:def 1;
reconsider F1 = F as FinSequence of REAL by Lm2;
thus Sum (F ^ <*r*>) = Sum (F1 ^ <*s*>)
.= addreal . ((addreal $$ F1),s) by FINSOP_1:4
.= (Sum F1) + r by BINOP_2:def 9
.= (Sum F) + r ; :: thesis: verum