let K be Field; :: 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:85; :: thesis: verum