defpred S₁[ Element of 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 ; :: thesis: ( ( 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 Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let f be FinSequence of NAT ; :: thesis: ( 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 ; :: thesis: ( 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:22;

A6: now

let i be Element of NAT ; :: thesis: ( i in dom g implies g . i <> 0 )
A7: dom g c= dom f by A5, FINSEQ_1:39;
assume A8: i in dom g ; :: thesis: g . i <> 0
then f . i = g . i by A5, FINSEQ_1:def 7;
hence g . i <> 0 by A4, A8, A7; :: thesis: verum

end;

n + 1 = (len g) + (len <*a*>) by A3, A5, FINSEQ_1:35;
then A9: n + 1 = (len g) + 1 by FINSEQ_1:57;
then ( dom f = Seg (len f) & f . (len f) = a ) by A3, A5, FINSEQ_1:59, FINSEQ_1:def 3;
then a <> 0 by A3, A4, FINSEQ_1:6;
then A10: 0 + 1 <= a by NAT_1:13;
A11: g is FinSequence of REAL by FINSEQ_2:27;

hereby :: thesis: ( f = (len f) |-> 1 implies Sum f = len f )

reconsider h = (len g) |-> 1 as FinSequence of REAL ;
reconsider h1 = h as Element of (len h) -tuples_on REAL by FINSEQ_2:110;
reconsider g1 = g as Element of (len g) -tuples_on REAL by A11, FINSEQ_2:110;
assume A12: Sum f = len f ; :: thesis: f = (len f) |-> 1
A13: Sum g = ((Sum g) + a) - a
.= (n + 1) - a by A3, A5, A12, RVSUM_1:104 ;

A14: now

let j be Nat; :: thesis: ( j in Seg (len g) implies h1 . j <= g1 . j )
reconsider a = j as Element of NAT by ORDINAL1:def 13;
assume A15: j in Seg (len g) ; :: thesis: h1 . j <= g1 . j
then j in dom g by FINSEQ_1:def 3;
then g . j <> 0 by A6;
then 0 + 1 <= g . a by NAT_1:13;
hence h1 . j <= g1 . j by A15, FUNCOP_1:13; :: thesis: verum

end;

len h1 = len g1 by FINSEQ_1:def 18;
then A16: Sum h1 <= Sum g1 by A14, RVSUM_1:112;
Sum h = n * 1 by A9, RVSUM_1:110
.= n ;
then n + a <= ((n + 1) - a) + a by A16, A13, XREAL_1:8;
then a <= 1 by XREAL_1:8;
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:74; :: thesis: verum

end;

assume f = (len f) |-> 1 ; :: thesis: Sum f = len f
then A18: f = (n |-> 1) ^ (1 |-> 1) by A3, FINSEQ_2:143
.= (n |-> 1) ^ <*1*> by FINSEQ_2:73 ;
then A19: a = 1 by A5, FINSEQ_2:20;
A20: Sum f = (Sum g) + a by A5, RVSUM_1:104;
g = (len g) |-> 1 by A5, A9, A18, FINSEQ_2:20;
hence Sum f = len f by A2, A3, A9, A6, A20, A19; :: thesis: verum

end;

A21: S₁[ 0 ]

proof

let f be FinSequence of NAT ; :: thesis: ( len f = 0 & ( 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
A22: len f = 0 and
for i being Element of NAT st i in dom f holds
f . i <> 0 ; :: thesis: ( Sum f = len f iff f = (len f) |-> 1 )

hereby :: thesis: ( f = (len f) |-> 1 implies Sum f = len f )

assume Sum f = len f ; :: thesis: f = (len f) |-> 1
thus f = {} by A22
.= (len f) |-> 1 by A22 ; :: thesis: verum

end;

assume f = (len f) |-> 1 ; :: thesis: Sum f = len f
f = {} by A22;
hence Sum f = len f by RVSUM_1:102; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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 ) ) ; :: thesis: verum