defpred S_{1}[ 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 S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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

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 S

S

proof

A21:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[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:19;

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;

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; :: thesis: verum

end;assume A2: S

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:19;

A6: now :: thesis: for i being Element of NAT st i in dom g holds

g . i <> 0

n + 1 = (len g) + (len <*a*>)
by A3, A5, FINSEQ_1:22;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 A5, FINSEQ_1:26;

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;A7: dom g c= dom f by A5, FINSEQ_1:26;

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

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 :: thesis: ( f = (len f) |-> 1 implies Sum f = len f )

assume
f = (len f) |-> 1
; :: thesis: Sum f = len freconsider 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 ; :: thesis: f = (len f) |-> 1

A13: Sum g = ((Sum g) + a) - a

.= (n + 1) - a by A3, A5, A12, RVSUM_1:74 ;

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; :: thesis: verum

end;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 ; :: thesis: f = (len f) |-> 1

A13: Sum g = ((Sum g) + a) - a

.= (n + 1) - a by A3, A5, A12, RVSUM_1:74 ;

A14: now :: thesis: for j being Nat st j in Seg (len g) holds

h1 . j <= g1 . j

A16:
Sum h1 <= Sum g1
by A14, RVSUM_1:82;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 A15, FUNCOP_1:7; :: thesis: verum

end;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 A15, FUNCOP_1:7; :: thesis: verum

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; :: thesis: verum

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; :: thesis: verum

proof

for n being Nat holds S
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;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

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