let i be Nat; :: thesis: for f being FinSequence of NAT st i in Seg (Sum f) holds
( (min f,i) -' 1 = (min f,i) - 1 & Sum (f | ((min f,i) -' 1)) < i )
let f be FinSequence of NAT ; :: thesis: ( i in Seg (Sum f) implies ( (min f,i) -' 1 = (min f,i) - 1 & Sum (f | ((min f,i) -' 1)) < i ) )
set F = min f,i;
assume A1: i in Seg (Sum f) ; :: thesis: ( (min f,i) -' 1 = (min f,i) - 1 & Sum (f | ((min f,i) -' 1)) < i )
then min f,i in dom f by Def1;
then 1 <= min f,i by FINSEQ_3:27;
hence A2: (min f,i) -' 1 = (min f,i) - 1 by XREAL_1:235; :: thesis: Sum (f | ((min f,i) -' 1)) < i
assume Sum (f | ((min f,i) -' 1)) >= i ; :: thesis: contradiction
then (min f,i) -' 1 >= (min f,i) - 0 by A1, Def1;
hence contradiction by A2, XREAL_1:12; :: thesis: verum