defpred S₁[ Element of NAT ] means for F being XFinSequence of NAT
for n being Element of NAT st dom F = $1 & rng F c= {0 ,n} holds
Sum F = n * (card (F " {n}));
let F be XFinSequence of NAT ; :: thesis: for n being Element of NAT st rng F c= {0 ,n} holds
Sum F = n * (card (F " {n}))
let n be Element of NAT ; :: thesis: ( rng F c= {0 ,n} implies Sum F = n * (card (F " {n})) )
assume A1: rng F c= {0 ,n} ; :: thesis: Sum F = n * (card (F " {n}))
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
let F be XFinSequence of NAT ; :: thesis: for n being Element of NAT st dom F = k + 1 & rng F c= {0 ,n} holds
Sum F = n * (card (F " {n}))
let n be Element of NAT ; :: thesis: ( dom F = k + 1 & rng F c= {0 ,n} implies Sum F = n * (card (F " {n})) )
assume that
A4: dom F = k + 1 and
A5: rng F c= {0 ,n} ; :: thesis: Sum F = n * (card (F " {n}))

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

suppose A6: n <> 0 ; :: thesis: Sum F = n * (card (F " {n}))

( not k in k & k \/ {k} = k + 1 ) by AFINSQ_1:4;
then A7: (dom F) \ {k} = k by A4, ZFMISC_1:141;
k < k + 1 by NAT_1:13;
then k in dom F by A4, NAT_1:45;
then A8: F . k in rng F by FUNCT_1:def 5;

per cases ( F . k = 0 or F . k = n ) by A5, A8, TARSKI:def 2;

suppose A9: F . k = 0 ; :: thesis: Sum F = n * (card (F " {n}))

A10: F | (k + 1) = F by A4, RELAT_1:98;
A11: k < k + 1 by NAT_1:13;
then k in dom F by A4, NAT_1:45;
then A12: (Sum (F | k)) + 0 = Sum F by A9, A10, Th44;
dom F = len F ;
then A13: len (F | k) = k by A4, A11, Lm2;
( rng (F | k) c= rng F & (F | k) " {n} = F " {n} ) by A6, A7, A9, Th15, RELAT_1:99;
hence Sum F = n * (card (F " {n})) by A3, A5, A13, A12, XBOOLE_1:1; :: thesis: verum

end;

suppose A14: F . k = n ; :: thesis: Sum F = n * (card (F " {n}))

set Fk = (F | k) " {n};
not k in k ;
then not k in (dom F) /\ k by XBOOLE_0:def 4;
then not k in dom (F | k) by RELAT_1:90;
then A15: not k in (F | k) " {n} by FUNCT_1:def 13;
A16: k < k + 1 by NAT_1:13;
then A17: k in dom F by A4, NAT_1:45;
dom F = len F ;
then ( rng (F | k) c= rng F & len (F | k) = k ) by A4, A16, Lm2, RELAT_1:99;
then A18: Sum (F | k) = n * (card ((F | k) " {n})) by A3, A5, XBOOLE_1:1;
F | (k + 1) = F by A4, RELAT_1:98;
then A19: (Sum (F | k)) + n = Sum F by A14, A17, Th44;
{k} \/ ((F | k) " {n}) = F " {n} by A7, A14, A17, Th13;
then (card ((F | k) " {n})) + 1 = card (F " {n}) by A15, CARD_2:54;
hence Sum F = n * (card (F " {n})) by A18, A19; :: thesis: verum

end;

end;

end;

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

for k being Element of NAT st k in dom F holds
F . k = 0

proof

let k be Element of NAT ; :: thesis: ( k in dom F implies F . k = 0 )
assume k in dom F ; :: thesis: F . k = 0
then F . k in rng F by FUNCT_1:def 5;
hence F . k = 0 by A5, A20, TARSKI:def 2; :: thesis: verum

end;

hence Sum F = n * (card (F " {n})) by A20, STIRL2_1:53; :: thesis: verum

end;

end;

end;

A21: S₁[ 0 ]

proof

let F be XFinSequence of NAT ; :: thesis: for n being Element of NAT st dom F = 0 & rng F c= {0 ,n} holds
Sum F = n * (card (F " {n}))
let n be Element of NAT ; :: thesis: ( dom F = 0 & rng F c= {0 ,n} implies Sum F = n * (card (F " {n})) )
assume that
A22: dom F = 0 and
rng F c= {0 ,n} ; :: thesis: Sum F = n * (card (F " {n}))
F " {n} c= 0 by A22, RELAT_1:167;
then A23: F " {n} = {} ;
len F = 0 by A22;
hence Sum F = n * (card (F " {n})) by A23, STIRL2_1:53; :: thesis: verum

end;

A24: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A21, A2);
ex k being Element of NAT st dom F = k by AFINSQ_1:7;
hence Sum F = n * (card (F " {n})) by A1, A24; :: thesis: verum