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:25;
hence A2: (min (f,i)) -' 1 = (min (f,i)) - 1 by XREAL_1:233; :: 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:10; :: thesis: verum