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) ) )
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) )
reconsider fg = f ^ g as FinSequence of NAT ;
A2: Sum fg = (Sum f) + (Sum g) by RVSUM_1:105;
then A3: i in Seg (Sum fg) by A1, XBOOLE_0:def 5;
then A4: i <= Sum (fg | (min fg,i)) by Def1;
not i in Seg (Sum f) by A1, XBOOLE_0:def 5;
then A5: ( 1 <= i & ( 1 > i or i > Sum f ) ) by A3, FINSEQ_1:3;
then reconsider j = i - (Sum f) as Element of NAT by NAT_1:21;
j <> 0 by A5;
then ( j > 0 & i = j + (Sum f) ) ;
then A6: j in Seg (Sum g) by A2, A3, FINSEQ_1:82;
min fg,i > len f

proof

assume min fg,i <= len f ; :: thesis: contradiction
then ( fg | (min fg,i) = f | (min fg,i) & Sum (f | (min fg,i)) <= Sum (f | (len f)) & f | (len f) = f ) by FINSEQ_1:79, FINSEQ_5:25, POLYNOM3:18;
hence contradiction by A5, A4, 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 A4, RVSUM_1:105;
then j <= ((Sum f) + (Sum (g | m))) - (Sum f) by XREAL_1:11;
then m >= min g,j by Def1, A6;
then A7: m + (len f) >= (min g,j) + (len f) by XREAL_1:9;
A8: j <= Sum (g | (min g,j)) by Def1, A6;
fg | ((len f) + (min g,j)) = f ^ (g | (min g,j)) by FINSEQ_6:16;
then Sum (fg | ((len f) + (min g,j))) = (Sum f) + (Sum (g | (min g,j))) by RVSUM_1:105;
then Sum (fg | ((len f) + (min g,j))) >= (Sum f) + j by A8, XREAL_1:9;
then (len f) + (min g,j) >= min fg,i by A3, Def1;
then ( (len f) + (min g,j) = min fg,i & j = i -' (Sum f) ) by A5, A7, XREAL_1:235, XXREAL_0:1;
hence ( min (f ^ g),i = (min g,(i -' (Sum f))) + (len f) & i -' (Sum f) = i - (Sum f) ) ; :: thesis: verum