let f be complex-valued FinSequence; :: 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 f = f as FinSequence of COMPLEX by RVSUM_1:146;
Sum (f + (- x)) = (Sum f) + ((- x) * (len f)) by SFX;
hence Sum (f - x) = (Sum f) - (x * (len f)) by VALUED_1:def 3; :: thesis: verum