let F be XFinSequence of ; :: 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}))
defpred S₁[ Element of NAT ] means for F being XFinSequence of
for n being Element of NAT st dom F = $1 & rng F c= {0 ,n} holds
Sum F = n * (card (F " {n}));
A2: S₁[ 0 ]

proof

let F be XFinSequence of ; :: 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
A3: dom F = 0 and
rng F c= {0 ,n} ; :: thesis: Sum F = n * (card (F " {n}))
F " {n} c= 0 by A3, RELAT_1:167;
then ( len F = 0 & F " {n} = {} & card {} = 0 ) by A3;
hence Sum F = n * (card (F " {n})) by STIRL2_1:53; :: thesis: verum

end;

A4: 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 A5: S₁[k] ; :: thesis: S₁[k + 1]
let F be XFinSequence of ; :: 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 A6: ( dom F = k + 1 & rng F c= {0 ,n} ) ; :: thesis: Sum F = n * (card (F " {n}))

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

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

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

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

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

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

end;

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

set Fk = (F | k) " {n};
k < k + 1 by NAT_1:13;
then A12: ( k in dom F & F | (k + 1) = F & k < dom F & dom F = len F & rng (F | k) c= rng F ) by A6, NAT_1:45, RELAT_1:98, RELAT_1:99;
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 ( not k in (F | k) " {n} & {k} \/ ((F | k) " {n}) = F " {n} & rng (F | k) c= {0 ,n} & len (F | k) = k ) by A6, A9, A11, A12, Lm2, Th13, FUNCT_1:def 13, XBOOLE_1:1;
then ( Sum (F | k) = n * (card ((F | k) " {n})) & (Sum (F | k)) + n = Sum F & (card ((F | k) " {n})) + 1 = card (F " {n}) & (n * (card ((F | k) " {n}))) + n = n * ((card ((F | k) " {n})) + 1) ) by A5, A11, A12, Th44, CARD_2:54;
hence Sum F = n * (card (F " {n})) ; :: thesis: verum

end;

end;

end;

suppose A13: 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 A6, A13, TARSKI:def 2; :: thesis: verum

end;

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

end;

end;

end;

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