let f, g be FinSequence of COMPLEX ; :: thesis: len (f - g) = min ((len f),(len g))
reconsider h = - g as FinSequence of COMPLEX by NEWTON02:103;
h = (- 1) (#) g by VALUED_1:def 6;
then dom h = dom g by VALUED_1:def 5;
then A1: len h = len g by FINSEQ_3:29;
f - g = f + h by VALUED_1:def 9;
hence len (f - g) = min ((len f),(len g)) by FLS, A1; :: thesis: verum