theorem :: CARDFIN2:13

for F being XFinSequence of INT
for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))