let K be Ring; :: thesis: for p, q being FinSequence of K holds len (mlt (p,q)) = min ((len p),(len q))
let p, q be FinSequence of K; :: thesis: 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; :: thesis: verum