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 ) by A1;
A3: Sum fg = (Sum f) + (Sum g) by RVSUM_1:105;
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:3, NAT_1:21;
A5: i = j + (Sum f) ;
fg | ((len f) + (min g,j)) = f ^ (g | (min g,j)) by FINSEQ_6:16;
then A6: Sum (fg | ((len f) + (min g,j))) = (Sum f) + (Sum (g | (min g,j))) by RVSUM_1:105;
j <> 0 by A4, A2, FINSEQ_1:3;
then A7: j in Seg (Sum g) by A3, A4, A5, FINSEQ_1:82;
then j <= Sum (g | (min g,j)) by Def1;
then Sum (fg | ((len f) + (min g,j))) >= (Sum f) + j by A6, XREAL_1:9;
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:79;
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:25;
hence contradiction by A4, A9, A2, A12, A10, FINSEQ_1:3, 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:16;
then i <= (Sum f) + (Sum (g | m)) by A9, RVSUM_1:105;
then j <= ((Sum f) + (Sum (g | m))) - (Sum f) by XREAL_1:11;
then m >= min g,j by A7, Def1;
then A13: m + (len f) >= (min g,j) + (len f) by XREAL_1:9;
j = i -' (Sum f) by A4, A2, FINSEQ_1:3, XREAL_1:235;
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