let f be FinSequence of NAT ; for i, j being Nat st i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) holds
i = j
A1:
now for i, j being Nat st i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) holds
not i > jlet i,
j be
Nat;
( i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) implies not i > j )assume that A2:
i <= len f
and
j <= len f
and A3:
Sum (f | i) = Sum (f | j)
and A4:
(
i in dom f implies
f . i <> 0 )
and
(
j in dom f implies
f . j <> 0 )
;
not i > jassume A5:
i > j
;
contradictionthen reconsider i1 =
i - 1 as
Element of
NAT by NAT_1:20;
A6:
i = i1 + 1
;
then
j <= i1
by A5, NAT_1:13;
then A7:
Sum (f | j) <= Sum (f | i1)
by POLYNOM3:18;
A8:
i >= 1
by A6, NAT_1:14;
then
i in dom f
by A2, FINSEQ_3:25;
then
f | (i1 + 1) = (f | i1) ^ <*(f . i)*>
by FINSEQ_5:10;
then A9:
Sum (f | j) = (Sum (f | i1)) + (f . i)
by A3, RVSUM_1:74;
then
Sum (f | i1) <= Sum (f | j)
by NAT_1:11;
then
Sum (f | i1) = Sum (f | j)
by A7, XXREAL_0:1;
hence
contradiction
by A2, A4, A8, A9, FINSEQ_3:25;
verum end;
let i, j be Nat; ( i <= len f & j <= len f & Sum (f | i) = Sum (f | j) & ( i in dom f implies f . i <> 0 ) & ( j in dom f implies f . j <> 0 ) implies i = j )
assume that
A10:
i <= len f
and
A11:
j <= len f
and
A12:
Sum (f | i) = Sum (f | j)
and
A13:
( i in dom f implies f . i <> 0 )
and
A14:
( j in dom f implies f . j <> 0 )
; i = j
A15:
j <= i
by A1, A10, A11, A12, A13, A14;
i <= j
by A1, A10, A11, A12, A13, A14;
hence
i = j
by A15, XXREAL_0:1; verum