let i be Nat; :: thesis: for c being Complex holds Sum (i |-> c) = i * c
let c be Complex; :: thesis: Sum (i |-> c) = i * c
reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
defpred S₁[ Nat] means Sum ($1 |-> c) = $1 * c;
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: Sum (i |-> c) = i * c ; :: thesis: S₁[i + 1]
thus Sum ((i + 1) |-> c) = Sum ((i |-> c) ^ <*c*>) by FINSEQ_2:60
.= (i * c) + (1 * c) by A2, Th31
.= (i + 1) * c ; :: thesis: verum

end;

A3: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A1);
hence Sum (i |-> c) = i * c ; :: thesis: verum