theorem DLS: :: NEWTON04:22

for f, g, h being FinSequence of COMPLEX st dom h = (dom f) /\ (dom g) holds
len h = min ((len f),(len g))