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);
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: 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 A5: dom cF = k + 1 ; :: thesis: c * (Sum cF) = Sum (c (#) cF)
set cF1 = c (#) cF;
A6: dom cF = dom (c (#) cF) by VALUED_1:def 5;
A7: for n being Nat holds c * (cF . n) = (c (#) cF) . n by VALUED_1:6;
reconsider cF = cF, cF1 = c (#) cF as XFinSequence of COMPLEX by Lm6;
A8: cF | (k + 1) = cF by A5, RELAT_1:98;
len cF = k + 1 by A5;
then A9: len (cF | k) = k by A4, AFINSQ_1:14;
k < k + 1 by NAT_1:13;
then A10: k in dom cF by A5, NAT_1:45;
then addcomplex . (addcomplex "**" (cF | k)),(cF . k) = addcomplex "**" (cF | (k + 1)) by Th56;
then A11: Sum cF = (Sum (cF | k)) + (cF . k) by A8, BINOP_2:def 3;
A15: c * (Sum (cF | k)) = Sum (c (#) (cF | k)) by A3, A9
.= Sum (cF1 | k) by TTT1 ;
k < k + 1 by NAT_1:13;
then k in dom cF by A5, NAT_1:45;
A16: c * (cF . k) = cF1 . k by VALUED_1:6;
A17: cF1 | (k + 1) = cF1 by A5, A6, RELAT_1:98;
addcomplex . (addcomplex "**" (cF1 | k)),(cF1 . k) = addcomplex "**" (cF1 | (k + 1)) by A6, A10, Th56;
then Sum cF1 = (Sum (cF1 | k)) + (cF1 . k) by A17, BINOP_2:def 3;
hence c * (Sum cF) = Sum (c (#) cF) by A11, A16, A15; :: thesis: verum

end;

A18: S₁[ 0 ]

proof

let cF be complex-valued XFinSequence; :: thesis: ( dom cF = 0 implies c * (Sum cF) = Sum (c (#) cF) )
assume A19: 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 Lm6;
len cF = 0 by A19;
then A21: addcomplex "**" cF = 0 by BINOP_2:1, Def9;
len cF1 = 0 by A19, VALUED_1:def 5;
hence c * (Sum cF) = Sum (c (#) cF) by A21, BINOP_2:1, Def9; :: thesis: verum

end;

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