theorem Th3: :: INT_6:3

for f1, f2 being complex-valued FinSequence holds len (f1 (#) f2) = min ((len f1),(len f2))