let f be FinSequence of COMPLEX ; :: thesis: for x being Complex holds Sum (f + x) = (Sum f) + (x * (len f))
let x be Complex; :: thesis: Sum (f + x) = (Sum f) + (x * (len f))
reconsider x = x as Element of COMPLEX by XCMPLX_0:def 2;
set k = len f;
set g = (len f) |-> x;
f null {} is len f -element ;
then reconsider f = f as len f -element FinSequence of COMPLEX ;
reconsider h = f + x as FinSequence of COMPLEX by RVSUM_1:146;
dom f = dom (f + x) by VALUED_1:def 2;
then len f = len (f + x) by FINSEQ_3:29;
then h null {} is len f -element ;
then reconsider h = h as len f -element FinSequence of COMPLEX ;
Sum (f + x) = Sum (f + ((len f) |-> x)) by SL
.= (Sum f) + (Sum ((len f) |-> x)) by RVSUM_2:40
.= (Sum f) + ((len f) * x) by RVSUM_2:36 ;
hence Sum (f + x) = (Sum f) + (x * (len f)) ; :: thesis: verum