let i be Nat; 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 ; ( 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))
; ( 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
;
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;
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; verum