let i be Nat; :: thesis: for f, g being FinSequence of NAT st i in (Seg ((Sum f) + (Sum g))) \ (Seg (Sum f)) holds
( min ((f ^ g),i) = (min (g,(i -' (Sum f)))) + (len f) & i -' (Sum f) = i - (Sum f) )
let f, g be FinSequence of NAT ; :: thesis: ( i in (Seg ((Sum f) + (Sum g))) \ (Seg (Sum f)) implies ( min ((f ^ g),i) = (min (g,(i -' (Sum f)))) + (len f) & i -' (Sum f) = i - (Sum f) ) )
reconsider fg = f ^ g as FinSequence of NAT ;
assume A1: i in (Seg ((Sum f) + (Sum g))) \ (Seg (Sum f)) ; :: thesis: ( min ((f ^ g),i) = (min (g,(i -' (Sum f)))) + (len f) & i -' (Sum f) = i - (Sum f) )
then not i in Seg (Sum f) by XBOOLE_0:def 5;
then A2: ( 1 > i or i > Sum f ) ;
A3: Sum fg = (Sum f) + (Sum g) by RVSUM_1:75;
then A4: i in Seg (Sum fg) by A1, XBOOLE_0:def 5;
then reconsider j = i - (Sum f) as Element of NAT by A2, FINSEQ_1:1, NAT_1:21;
A5: i = j + (Sum f) ;
fg | ((len f) + (min (g,j))) = f ^ (g | (min (g,j))) by FINSEQ_6:14;
then A6: Sum (fg | ((len f) + (min (g,j)))) = (Sum f) + (Sum (g | (min (g,j)))) by RVSUM_1:75;
j <> 0 by A4, A2, FINSEQ_1:1;
then A7: j in Seg (Sum g) by A3, A4, A5, FINSEQ_1:61;
then j <= Sum (g | (min (g,j))) by Def1;
then Sum (fg | ((len f) + (min (g,j)))) >= (Sum f) + j by A6, XREAL_1:7;
then A8: (len f) + (min (g,j)) >= min (fg,i) by A4, Def1;
A9: i <= Sum (fg | (min (fg,i))) by A4, Def1;
min (fg,i) > len f

proof

A10: f | (len f) = f by FINSEQ_1:58;
assume A11: min (fg,i) <= len f ; :: thesis: contradiction
then A12: Sum (f | (min (fg,i))) <= Sum (f | (len f)) by POLYNOM3:18;
fg | (min (fg,i)) = f | (min (fg,i)) by A11, FINSEQ_5:22;
hence contradiction by A4, A9, A2, A12, A10, FINSEQ_1:1, XXREAL_0:2; :: thesis: verum

end;

then reconsider m = (min (fg,i)) - (len f) as Element of NAT by NAT_1:21;
fg | ((len f) + m) = f ^ (g | m) by FINSEQ_6:14;
then i <= (Sum f) + (Sum (g | m)) by A9, RVSUM_1:75;
then j <= ((Sum f) + (Sum (g | m))) - (Sum f) by XREAL_1:9;
then m >= min (g,j) by A7, Def1;
then A13: m + (len f) >= (min (g,j)) + (len f) by XREAL_1:7;
j = i -' (Sum f) by A4, A2, FINSEQ_1:1, XREAL_1:233;
hence ( min ((f ^ g),i) = (min (g,(i -' (Sum f)))) + (len f) & i -' (Sum f) = i - (Sum f) ) by A13, A8, XXREAL_0:1; :: thesis: verum