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 ; :: 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 Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[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 ;
A6: now :: thesis: for i being Element of NAT st i in dom g holds
g . i <> 0
let i be Element of NAT ; :: thesis: ( i in dom g implies g . i <> 0 )
A7: dom g c= dom f by ;
assume A8: i in dom g ; :: thesis: g . i <> 0
then f . i = g . i by ;
hence g . i <> 0 by A4, A8, A7; :: thesis: verum
end;
n + 1 = (len g) + () by ;
then A9: n + 1 = (len g) + 1 by FINSEQ_1:40;
then ( dom f = Seg (len f) & f . (len f) = a ) by ;
then a <> 0 by ;
then A10: 0 + 1 <= a by NAT_1:13;
A11: g is FinSequence of REAL by ;
hereby :: thesis: ( 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 ;
assume A12: Sum f = len f ; :: thesis: f = (len f) |-> 1
A13: Sum g = ((Sum g) + a) - a
.= (n + 1) - a by ;
A14: now :: thesis: for j being Nat st j in Seg (len g) holds
h1 . j <= g1 . j
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 12;
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 ; :: thesis: verum
end;
A16: Sum h1 <= Sum g1 by ;
Sum h = n * 1 by
.= n ;
then n + a <= ((n + 1) - a) + a by ;
then a <= 1 by XREAL_1:6;
then A17: a = 1 by ;
then g = (len g) |-> 1 by A2, A9, A6, A13;
hence f = (len f) |-> 1 by ; :: thesis: verum
end;
assume f = (len f) |-> 1 ; :: thesis: Sum f = len f
then A18: f = (n |-> 1) ^ (1 |-> 1) by
.= (n |-> 1) ^ <*1*> by FINSEQ_2:59 ;
then A19: a = 1 by ;
A20: Sum f = (Sum g) + a by ;
g = (len g) |-> 1 by ;
hence Sum f = len f by A2, A3, A9, A6, A20, A19; :: thesis: verum
end;
A21: S1[ 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 )
thus ( Sum f = len f implies f = (len f) |-> 1 ) by A22; :: thesis: ( f = (len f) |-> 1 implies Sum f = len f )
assume f = (len f) |-> 1 ; :: thesis: Sum f = len f
f = {} by A22;
hence Sum f = len f by RVSUM_1:72; :: thesis: verum
end;
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 ) ) ; :: thesis: verum