let r be Real; :: thesis: for f being real-valued FinSequence st rng f c= {0,r} holds
Sum f = r * (card (f " {r}))
defpred S₁[ Nat] means for f being real-valued FinSequence st len f = $1 & rng f c= {0,r} holds
Sum f = r * (card (f " {r}));
A1: S₁[ 0 ]

proof

let f be real-valued FinSequence; :: thesis: ( len f = 0 & rng f c= {0,r} implies Sum f = r * (card (f " {r})) )
assume that
A2: len f = 0 and
rng f c= {0,r} ; :: thesis: Sum f = r * (card (f " {r}))
A3: f = {} by A2;
then f " {r} = {} ;
hence Sum f = r * (card (f " {r})) by A3, RVSUM_1:72; :: thesis: verum

end;

A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
let f be real-valued FinSequence; :: thesis: ( len f = n + 1 & rng f c= {0,r} implies Sum f = r * (card (f " {r})) )
assume that
A6: len f = n + 1 and
A7: rng f c= {0,r} ; :: thesis: Sum f = r * (card (f " {r}))
rng f c= REAL ;
then reconsider F = f as FinSequence of REAL by FINSEQ_1:def 4;
set fn = F | n;
set FF = <*(f . (n + 1))*>;
A8: f = (F | n) ^ <*(f . (n + 1))*> by A6, FINSEQ_3:55;
then A9: Sum f = (Sum (F | n)) + (F . (n + 1)) by RVSUM_1:74;
rng (F | n) c= rng f by RELAT_1:70;
then A10: rng (F | n) c= {0,r} by A7;
A11: len (F | n) = n by NAT_1:11, A6, FINSEQ_1:59;
then A12: Sum (F | n) = r * (card ((F | n) " {r})) by A10, A5;
A13: dom <*(f . (n + 1))*> = Seg 1 by FINSEQ_1:38;
rng <*(f . (n + 1))*> = {(F . (n + 1))} by FINSEQ_1:38;
then A14: <*(f . (n + 1))*> = (Seg 1) --> (F . (n + 1)) by A13, FUNCOP_1:9;
A15: card (f " {r}) = (card ((F | n) " {r})) + (card (<*(f . (n + 1))*> " {r})) by FINSEQ_3:57, A8;
1 <= n + 1 by NAT_1:11;
then n + 1 in dom F by A6, FINSEQ_3:25;
then A16: F . (n + 1) in rng F by FUNCT_1:def 3;

per cases ( F . (n + 1) <> r or F . (n + 1) = r ) ;

suppose A17: F . (n + 1) <> r ; :: thesis: Sum f = r * (card (f " {r}))

then not F . (n + 1) in {r} by TARSKI:def 1;
then A18: <*(f . (n + 1))*> " {r} = {} by A14, FUNCOP_1:16;
F . (n + 1) = 0 by A17, A16, A7, TARSKI:def 2;
hence Sum f = r * (card (f " {r})) by A11, A10, A5, A9, A15, A18; :: thesis: verum

end;

suppose A19: F . (n + 1) = r ; :: thesis: Sum f = r * (card (f " {r}))

then <*(f . (n + 1))*> " {r} = Seg 1 by A14, FUNCOP_1:15;
then card (<*(f . (n + 1))*> " {r}) = 1 by FINSEQ_1:57;
hence Sum f = r * (card (f " {r})) by A12, A9, A15, A19; :: thesis: verum

end;

end;

end;

A20: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A4);
let f be real-valued FinSequence; :: thesis: ( rng f c= {0,r} implies Sum f = r * (card (f " {r})) )
S₁[ len f] by A20;
hence ( rng f c= {0,r} implies Sum f = r * (card (f " {r})) ) ; :: thesis: verum