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: ( len cF = k + 1 implies c * (Sum cF) = Sum (c (#) cF) )
assume A4: len 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 Lm2;
A6: cF | (k + 1) = cF by A4;
A7: len (cF | k) = k by A3, AFINSQ_1:11, A4;
k < k + 1 by NAT_1:13;
then A8: k in dom cF by A4, AFINSQ_1:86;
then addcomplex . ((addcomplex "**" (cF | k)),(cF . k)) = addcomplex "**" (cF | (k + 1)) by Th42;
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 Th62 ;
A11: c * (cF . k) = cF1 . k by VALUED_1:6;
A12: cF1 | (k + 1) = cF1 by A4, A5;
addcomplex . ((addcomplex "**" (cF1 | k)),(cF1 . k)) = addcomplex "**" (cF1 | (k + 1)) by A5, A8, Th42;
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

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