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 that
A1: len F1 = len F2 and
A2: len F2 = len F3 ; :: thesis: mlt F1,(mlt F2,F3) = mlt (mlt F1,F2),F3
reconsider f3 = F3 as Element of (len F3) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider f2 = F2 as Element of (len F2) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider f1 = F1 as Element of (len F1) -tuples_on COMPLEX by FINSEQ_2:110;
thus mlt F1,(mlt F2,F3) = multcomplex .: (multcomplex .: f1,f2),f3 by A1, A2, FINSEQOP:29
.= mlt (mlt F1,F2),F3 ; :: thesis: verum