let f, g be FinSequence of COMPLEX ; :: thesis: len (f (#) g) = min ((len f),(len g))
reconsider h = f (#) g as FinSequence of COMPLEX by NEWTON02:103;
dom h = (dom f) /\ (dom g) by VALUED_1:def 4;
hence len (f (#) g) = min ((len f),(len g)) by DLS; :: thesis: verum