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 ) )
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 );
A1: 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
A2: 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 A2
.= (len f) |-> 1 by A2 ; :: thesis: verum

end;

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

end;

A3: 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 A4: 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
A5: len f = n + 1 and
A6: 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
A7: f = g ^ <*a*> by A5, FINSEQ_2:22;
A8: g is FinSequence of REAL by FINSEQ_2:27;
n + 1 = (len g) + (len <*a*>) by A5, A7, FINSEQ_1:35;
then A9: n + 1 = (len g) + 1 by FINSEQ_1:57;

A10: now

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

end;

A13: Sum f = (Sum g) + a by A7, RVSUM_1:104;
A14: dom f = Seg (len f) by FINSEQ_1:def 3;
f . (len f) = a by A5, A7, A9, FINSEQ_1:59;
then a <> 0 by A5, A6, A14, FINSEQ_1:6;
then A15: 0 + 1 <= a by NAT_1:13;

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

assume A16: Sum f = len f ; :: thesis: f = (len f) |-> 1
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 A8, FINSEQ_2:110;
A17: len h1 = len g1 by FINSEQ_1:def 18;

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 A18: 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 A10;
then 0 + 1 <= g . a by NAT_1:13;
hence h1 . j <= g1 . j by A18, FUNCOP_1:13; :: thesis: verum

end;

then A19: Sum h1 <= Sum g1 by A17, RVSUM_1:112;
A20: Sum h = n * 1 by A9, RVSUM_1:110
.= n ;
A21: Sum g = ((Sum g) + a) - a
.= (n + 1) - a by A5, A7, A16, RVSUM_1:104 ;
then n + a <= ((n + 1) - a) + a by A19, A20, XREAL_1:8;
then a <= 1 by XREAL_1:8;
then A22: a = 1 by A15, XXREAL_0:1;
then g = (len g) |-> 1 by A4, A9, A10, A21;
hence f = (len f) |-> 1 by A5, A7, A9, A22, FINSEQ_2:74; :: thesis: verum

end;

assume f = (len f) |-> 1 ; :: thesis: Sum f = len f
then f = (n |-> 1) ^ (1 |-> 1) by A5, FINSEQ_2:143
.= (n |-> 1) ^ <*1*> by FINSEQ_2:73 ;
then ( g = (len g) |-> 1 & a = 1 ) by A7, A9, FINSEQ_2:20;
hence Sum f = len f by A4, A5, A9, A10, A13; :: thesis: verum

end;

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