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_{1}[ Nat] means Sum ($1 |-> c) = $1 * c;

A1: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A3, A1);

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

let c be Complex; :: thesis: Sum (i |-> c) = i * c

reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;

defpred S

A1: for i being Nat st S

S

proof

A3:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: Sum (i |-> c) = i * c ; :: thesis: S_{1}[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;assume A2: Sum (i |-> c) = i * c ; :: thesis: S

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

for i being Nat holds S

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