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 Lm2;
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:92;
reconsider y9 = y1 as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x1 as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
x + (y + z) = addcomplex .: (x1,(y1 + z1)) by SEQ_4:def 6
.= addcomplex .: (x1,(addcomplex .: (y1,z1))) by SEQ_4:def 6
.= addcomplex .: ((addcomplex .: (x9,y9)),z9) by A1, FINSEQOP:28
.= addcomplex .: ((x1 + y1),z1) by SEQ_4:def 6
.= (x + y) + z by SEQ_4:def 6 ;
hence x + (y + z) = (x + y) + z ; :: thesis: verum