theorem FDX: :: RVSUM_4:31

for f being FinSequence
for g being XFinSequence
for x being Nat holds
( x in dom (f ^ g) iff ( x in dom f or x - ((len f) + 1) in dom g ) )