theorem Th4: :: MEASURE9:6

for D being set
for Y being FinSequenceSet of D
for F1, F2 being FinSequence of Y holds Length (F1 ^ F2) = (Length F1) ^ (Length F2)