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 Lm3;
A1: dom Fn = n by FUNCOP_1:13;

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 A2: dom Fn > 0 ; :: thesis: Sum (n --> c) = n * c

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

proof

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

end;

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

proof

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

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A11, A6);
hence Sum (n --> c) = n * c by A5, A10, A1; :: thesis: verum

end;

end;

end;

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