let x, y, z be complex-valued FinSequence; :: thesis: ( len x = len y & len y = len z implies x + (y + z) = (x + y) + z )
reconsider x1 = x, y1 = y, z1 = z as FinSequence of COMPLEX by Lm4;
assume A1: ( len x = len y & len y = len z ) ; :: thesis: x + (y + z) = (x + y) + z
reconsider z9 = z1 as Element of (len z) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
x + (y + z) = addcomplex .: x1,(y1 + z1) by SEQ_4:def 9
.= addcomplex .: x1,(addcomplex .: y1,z1) by SEQ_4:def 9
.= addcomplex .: (addcomplex .: x9,y9),z9 by A1, FINSEQOP:29
.= addcomplex .: (x1 + y1),z1 by SEQ_4:def 9
.= (x + y) + z by SEQ_4:def 9 ;
hence x + (y + z) = (x + y) + z ; :: thesis: verum