theorem Th2: :: INT_6:2

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