let F1, F2, F3 be FinSequence of COMPLEX ; :: thesis: ( len F1 = len F2 & len F2 = len F3 implies mlt F1,(mlt F2,F3) = mlt (mlt F1,F2),F3 )
assume A1: ( len F1 = len F2 & len F2 = len F3 ) ; :: thesis: mlt F1,(mlt F2,F3) = mlt (mlt F1,F2),F3
reconsider f1 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider f2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider f3 = F3 as Element of (len F3) -tuples_on COMPLEX by FINSEQ_2:110;
thus mlt F1,(mlt F2,F3) = multcomplex .: (multcomplex .: f1,f2),f3 by A1, FINSEQOP:29
.= mlt (mlt F1,F2),F3 ; :: thesis: verum