theorem :: RVSUM_4:34

for f being FinSequence
for g being XFinSequence holds dom (f \/ (Shift (g,((len f) + 1)))) = Seg ((len f) + (len g))