let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies x + (y + z) = (x + y) + z )
assume A1: ( len x = len y & len y = len z ) ; :: thesis: x + (y + z) = (x + y) + z
reconsider x' = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider y' = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider z' = z as Element of (len z) -tuples_on COMPLEX by FINSEQ_2:110;
x + (y + z) = addcomplex .: x,(y + z) by COMPLSP1:def 7
.= addcomplex .: x,(addcomplex .: y,z) by COMPLSP1:def 7
.= addcomplex .: (addcomplex .: x',y'),z' by A1, FINSEQOP:29
.= addcomplex .: (x + y),z by COMPLSP1:def 7
.= (x + y) + z by COMPLSP1:def 7 ;
hence x + (y + z) = (x + y) + z ; :: thesis: verum