let K be Field; :: thesis: for p, q being FinSequence of st len p = len q holds
( len (mlt p,q) = len p & len (mlt p,q) = len q )
let p, q be FinSequence of ; :: thesis: ( len p = len q implies ( len (mlt p,q) = len p & len (mlt p,q) = len q ) )
reconsider r = mlt p,q as FinSequence of ;
A1: r = the multF of K .: p,q by FVSUM_1:def 7;
assume len p = len q ; :: thesis: ( len (mlt p,q) = len p & len (mlt p,q) = len q )
hence ( len (mlt p,q) = len p & len (mlt p,q) = len q ) by A1, FINSEQ_2:86; :: thesis: verum