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