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