defpred S1[ Nat] means for f being FinSequence of NAT st len f = $1 & ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 );
let f be FinSequence of NAT ; ( ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let f be
FinSequence of
NAT ;
( len f = n + 1 & ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
assume that A3:
len f = n + 1
and A4:
for
i being
Element of
NAT st
i in dom f holds
f . i <> 0
;
( Sum f = len f iff f = (len f) |-> 1 )
consider g being
FinSequence of
NAT ,
a being
Element of
NAT such that A5:
f = g ^ <*a*>
by A3, FINSEQ_2:19;
n + 1
= (len g) + (len <*a*>)
by A3, A5, FINSEQ_1:22;
then A9:
n + 1
= (len g) + 1
by FINSEQ_1:40;
then
(
dom f = Seg (len f) &
f . (len f) = a )
by A3, A5, FINSEQ_1:42, FINSEQ_1:def 3;
then
a <> 0
by A3, A4, FINSEQ_1:4;
then A10:
0 + 1
<= a
by NAT_1:13;
A11:
g is
FinSequence of
REAL
by FINSEQ_2:24, NUMBERS:19;
hereby ( f = (len f) |-> 1 implies Sum f = len f )
reconsider h =
(len g) |-> jj as
FinSequence of
REAL ;
reconsider h1 =
h as
Element of
(len h) -tuples_on REAL by FINSEQ_2:92;
reconsider g1 =
g as
Element of
(len g) -tuples_on REAL by A11, FINSEQ_2:92;
assume A12:
Sum f = len f
;
f = (len f) |-> 1A13:
Sum g =
((Sum g) + a) - a
.=
(n + 1) - a
by A3, A5, A12, RVSUM_1:74
;
A16:
Sum h1 <= Sum g1
by A14, RVSUM_1:82;
Sum h =
n * 1
by A9, RVSUM_1:80
.=
n
;
then
n + a <= ((n + 1) - a) + a
by A16, A13, XREAL_1:6;
then
a <= 1
by XREAL_1:6;
then A17:
a = 1
by A10, XXREAL_0:1;
then
g = (len g) |-> 1
by A2, A9, A6, A13;
hence
f = (len f) |-> 1
by A3, A5, A9, A17, FINSEQ_2:60;
verum
end;
assume
f = (len f) |-> 1
;
Sum f = len f
then A18:
f =
(n |-> 1) ^ (1 |-> 1)
by A3, FINSEQ_2:123
.=
(n |-> 1) ^ <*1*>
by FINSEQ_2:59
;
then A19:
a = 1
by A5, FINSEQ_2:17;
A20:
Sum f = (Sum g) + a
by A5, RVSUM_1:74;
g = (len g) |-> 1
by A5, A9, A18, FINSEQ_2:17;
hence
Sum f = len f
by A2, A3, A9, A6, A20, A19;
verum
end;
A21:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A21, A1);
hence
( ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) implies ( Sum f = len f iff f = (len f) |-> 1 ) )
; verum