theorem Th1: :: INT_6:1

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