theorem XL1: :: RVSUM_4:29

for f being XFinSequence
for g being FinSequence holds
( len (f ^ g) = (len f) + (len g) & len (g ^ f) = (len f) + (len g) )