let f be complex-valued FinSequence; :: thesis: for c being Complex holds Sum (c + f) = (c * (len f)) + (Sum f)
let c be Complex; :: thesis: Sum (c + f) = (c * (len f)) + (Sum f)
defpred S₁[ complex-valued FinSequence] means Sum (c + $1) = (c * (len $1)) + (Sum $1);
A1: S₁[ <*> COMPLEX] ;
A2: for p being FinSequence of COMPLEX
for x being Element of COMPLEX st S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of COMPLEX ; :: thesis: for x being Element of COMPLEX st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of COMPLEX ; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A3: Sum (c + p) = (c * (len p)) + (Sum p) ; :: thesis: S₁[p ^ <*x*>]
set g = p ^ <*x*>;
A4: len <*x*> = 1 by FINSEQ_1:39;
A5: len (p ^ <*x*>) = (len p) + (len <*x*>) by FINSEQ_1:22;
A6: c + <*x*> = <*(c + x)*> by Th2;
A7: Sum (p ^ <*x*>) = (Sum p) + (Sum <*x*>) by RVSUM_2:32;
c + (p ^ <*x*>) = (c + p) ^ (c + <*x*>) by Th3;
hence Sum (c + (p ^ <*x*>)) = (Sum (c + p)) + (Sum (c + <*x*>)) by RVSUM_2:32
.= (c * (len (p ^ <*x*>))) + (Sum (p ^ <*x*>)) by A3, A4, A5, A6, A7 ;
:: thesis: verum

end;

A8: for p being FinSequence of COMPLEX holds S₁[p] from FINSEQ_2:sch 2(A1, A2);
f is FinSequence of COMPLEX by RVSUM_1:146;
hence Sum (c + f) = (c * (len f)) + (Sum f) by A8; :: thesis: verum