theorem Th9: :: MATRIXJ1:9

for i being 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) )