let K be Ring; for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))
let p, q be FinSequence of K; len (mlt (p,q)) = min ((len p),(len q))
reconsider r = mlt (p,q) as FinSequence of K ;
r = the multF of K .: (p,q)
by FVSUM_1:def 7;
hence
len (mlt (p,q)) = min ((len p),(len q))
by FINSEQ_2:71; verum