theorem Th15: :: MEASURE9:17

for D being non empty set
for Y being FinSequenceSet of D
for F being FinSequence of Y holds rng (joined_FinSeq F) = union { (rng (F . n)) where n is Nat : n in dom F }