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