let cF be complex-valued XFinSequence; :: thesis: for c being complex number holds c * (Sum cF) = Sum (c (#) cF)
let c be complex number ; :: thesis: c * (Sum cF) = Sum (c (#) cF)
defpred S₁[ Nat] means for cF being complex-valued XFinSequence st dom cF = $1 holds
c * (Sum cF) = Sum (c (#) cF);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
A3: k < k + 1 by NAT_1:13;
let cF be complex-valued XFinSequence; :: thesis: ( dom cF = k + 1 implies c * (Sum cF) = Sum (c (#) cF) )
assume A4: dom cF = k + 1 ; :: thesis: c * (Sum cF) = Sum (c (#) cF)
set cF1 = c (#) cF;
A5: dom cF = dom (c (#) cF) by VALUED_1:def 5;
reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3;
A6: cF | (k + 1) = cF by A4, RELAT_1:69;
len cF = k + 1 by A4;
then A7: len (cF | k) = k by A3, AFINSQ_1:11;
k < k + 1 by NAT_1:13;
then A8: k in dom cF by A4, NAT_1:44;
then addcomplex . ((addcomplex "**" (cF | k)),(cF . k)) = addcomplex "**" (cF | (k + 1)) by Th55;
then A9: Sum cF = (Sum (cF | k)) + (cF . k) by A6, BINOP_2:def 3;
A10: c * (Sum (cF | k)) = Sum (c (#) (cF | k)) by A2, A7
.= Sum (cF1 | k) by Th75 ;
A11: c * (cF . k) = cF1 . k by VALUED_1:6;
A12: cF1 | (k + 1) = cF1 by A4, A5, RELAT_1:69;
addcomplex . ((addcomplex "**" (cF1 | k)),(cF1 . k)) = addcomplex "**" (cF1 | (k + 1)) by A5, A8, Th55;
then Sum cF1 = (Sum (cF1 | k)) + (cF1 . k) by A12, BINOP_2:def 3;
hence c * (Sum cF) = Sum (c (#) cF) by A9, A11, A10; :: thesis: verum

end;

A13: S₁[ 0 ]

proof

let cF be complex-valued XFinSequence; :: thesis: ( dom cF = 0 implies c * (Sum cF) = Sum (c (#) cF) )
assume A14: dom cF = 0 ; :: thesis: c * (Sum cF) = Sum (c (#) cF)
set cF1 = c (#) cF;
reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm3;
len cF = 0 by A14;
then A15: addcomplex "**" cF = 0 by Def9, BINOP_2:1;
len cF1 = 0 by A14, VALUED_1:def 5;
hence c * (Sum cF) = Sum (c (#) cF) by A15, Def9, BINOP_2:1; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A13, A1);
then S₁[ len cF] ;
hence c * (Sum cF) = Sum (c (#) cF) ; :: thesis: verum