theorem FRX: :: RVSUM_4:32

for f being FinSequence
for g being XFinSequence holds
( rng (f ^ g) = (rng f) \/ (rng g) & rng (g ^ f) = (rng f) \/ (rng g) )