let cF be complex-valued XFinSequence; for c being Complex st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))
let c be Complex; ( rng cF c= {0,c} implies Sum cF = c * (card (cF " {c})) )
defpred S1[ Nat] means for cF being complex-valued XFinSequence
for c being Complex st len cF = $1 & rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}));
assume A1:
rng cF c= {0,c}
; Sum cF = c * (card (cF " {c}))
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
let F be
complex-valued XFinSequence;
for c being Complex st len F = k + 1 & rng F c= {0,c} holds
Sum F = c * (card (F " {c}))let c be
Complex;
( len F = k + 1 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) )
assume that A4:
len F = k + 1
and A5:
rng F c= {0,c}
;
Sum F = c * (card (F " {c}))
per cases
( c <> 0 or c = 0 )
;
suppose A6:
c <> 0
;
Sum F = c * (card (F " {c}))
( not
k in k &
(Segm k) \/ {k} = Segm (k + 1) )
by AFINSQ_1:2;
then A7:
(dom F) \ {k} = k
by A4, ZFMISC_1:117;
k < k + 1
by NAT_1:13;
then
k in dom F
by A4, AFINSQ_1:86;
then A8:
F . k in rng F
by FUNCT_1:def 3;
per cases
( F . k = 0 or F . k = c )
by A5, A8, TARSKI:def 2;
suppose A9:
F . k = 0
;
Sum F = c * (card (F " {c}))A10:
F | (k + 1) = F
by A4;
A11:
k < k + 1
by NAT_1:13;
then A12:
(Sum (F | k)) + 0 = Sum F
by A9, A10, Th64, A4, AFINSQ_1:86;
A13:
len (F | k) = k
by A4, A11, AFINSQ_1:54;
(
rng (F | k) c= rng F &
(F | k) " {c} = F " {c} )
by A6, A7, A9, Th66;
hence
Sum F = c * (card (F " {c}))
by A3, A5, A13, A12, XBOOLE_1:1;
verum end; suppose A14:
F . k = c
;
Sum F = c * (card (F " {c}))set Fk =
(F | k) " {c};
not
k in k
;
then
not
k in dom (F | k)
;
then A15:
not
k in (F | k) " {c}
by FUNCT_1:def 7;
A16:
k < k + 1
by NAT_1:13;
then A17:
k in dom F
by A4, AFINSQ_1:86;
(
rng (F | k) c= rng F &
len (F | k) = k )
by A4, A16, AFINSQ_1:54;
then A18:
Sum (F | k) = c * (card ((F | k) " {c}))
by A3, A5, XBOOLE_1:1;
F | (k + 1) = F
by A4;
then A19:
(Sum (F | k)) + c = Sum F
by A14, A17, Th64;
{k} \/ ((F | k) " {c}) = F " {c}
by A7, A14, A17, Th65;
then
(card ((F | k) " {c})) + 1
= card (F " {c})
by A15, CARD_2:41;
hence
Sum F = c * (card (F " {c}))
by A18, A19;
verum end; end; end; end;
end;
A21:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(A21, A2);
then
S1[ len cF]
;
hence
Sum cF = c * (card (cF " {c}))
by A1; verum