let n be Nat; :: thesis: for c being complex number holds Sum (n --> c) = n * c
let c be complex number ; :: thesis: Sum (n --> c) = n * c
set Fn = n --> c;
reconsider Fn = n --> c as XFinSequence of COMPLEX by Lm6;
A1: dom Fn = n by FUNCOP_1:19;

now

per cases ( dom Fn = 0 or dom Fn > 0 ) ;

suppose dom Fn = 0 ; :: thesis: Sum (n --> c) = n * c

hence Sum (n --> c) = n * c by A1; :: thesis: verum

end;

suppose A4: dom Fn > 0 ; :: thesis: Sum (n --> c) = n * c

then consider f being Function of NAT,COMPLEX such that
A5: f . 0 = Fn . 0 and
A6: for k being Nat st k + 1 < len Fn holds
f . (k + 1) = addcomplex . ((f . k),(Fn . (k + 1))) and
A7: Sum Fn = f . ((len Fn) - 1) by Def9;
defpred S₁[ Nat] means ( $1 < len Fn implies f . $1 = ($1 + 1) * c );
A8: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A9: S₁[m] ; :: thesis: S₁[m + 1]
assume A10: m + 1 < len Fn ; :: thesis: f . (m + 1) = ((m + 1) + 1) * c
then f . (m + 1) = addcomplex . ((f . m),(Fn . (m + 1))) by A6;
then A11: f . (m + 1) = (f . m) + (Fn . (m + 1)) by BINOP_2:def 3;
m + 1 in len Fn by A10, NAT_1:45;
then Fn . (m + 1) = c by A1, FUNCOP_1:13;
hence f . (m + 1) = ((m + 1) + 1) * c by A9, A10, A11, NAT_1:13; :: thesis: verum

end;

reconsider lenFn1 = (len Fn) - 1 as Element of NAT by A4, NAT_1:20;
A12: lenFn1 < lenFn1 + 1 by NAT_1:13;
A13: S₁[ 0 ]

proof

assume 0 < len Fn ; :: thesis: f . 0 = (0 + 1) * c
then 0 in dom Fn by NAT_1:45;
hence f . 0 = (0 + 1) * c by A5, FUNCOP_1:13, A1; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A13, A8);
hence Sum (n --> c) = n * c by A7, A12, A1; :: thesis: verum

end;

end;

end;

hence Sum (n --> c) = n * c ; :: thesis: verum