let cF be complex-valued XFinSequence; :: thesis: for c being Complex st rng cF c= {0,c} holds
Sum cF = c * (card (cF " {c}))
let c be Complex; :: thesis: ( rng cF c= {0,c} implies Sum cF = c * (card (cF " {c})) )
defpred S₁[ 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} ; :: thesis: Sum cF = c * (card (cF " {c}))
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let F be complex-valued XFinSequence; :: thesis: 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; :: thesis: ( 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} ; :: thesis: Sum F = c * (card (F " {c}))

per cases ( c <> 0 or c = 0 ) ;

suppose A6: c <> 0 ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A14: F . k = c ; :: thesis: 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; :: thesis: verum

end;

end;

end;

suppose A20: c = 0 ; :: thesis: Sum F = c * (card (F " {c}))

for x being object st x in dom F holds
F . x = 0

proof

let x be object ; :: thesis: ( x in dom F implies F . x = 0 )
assume x in dom F ; :: thesis: F . x = 0
then F . x in rng F by FUNCT_1:def 3;
hence F . x = 0 by A5, A20, TARSKI:def 2; :: thesis: verum

end;

then F = (dom F) --> 0 by FUNCOP_1:11;
then Sum F = (len F) * 0 by Th61;
hence Sum F = c * (card (F " {c})) by A20; :: thesis: verum

end;

end;

end;

A21: S₁[ 0 ]

proof

let F be complex-valued XFinSequence; :: thesis: for c being Complex st len F = 0 & rng F c= {0,c} holds
Sum F = c * (card (F " {c}))
let c be Complex; :: thesis: ( len F = 0 & rng F c= {0,c} implies Sum F = c * (card (F " {c})) )
assume that
A22: len F = 0 and
rng F c= {0,c} ; :: thesis: Sum F = c * (card (F " {c}))
( F " {c} c= 0 & F = {} ) by A22, RELAT_1:132;
then ( card (F " {c}) = 0 & Sum F = 0 ) ;
hence Sum F = c * (card (F " {c})) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A21, A2);
then S₁[ len cF] ;
hence Sum cF = c * (card (cF " {c})) by A1; :: thesis: verum