let x1, x2 be complex-valued FinSequence; :: thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 )

set n = len x1;

A1: x2 is FinSequence of COMPLEX by Lm2;

x1 is FinSequence of COMPLEX by Lm2;

then reconsider z1 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;

assume len x1 = len x2 ; :: thesis: len (x1 + x2) = len x1

then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;

dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124;

hence len (x1 + x2) = len x1 by FINSEQ_1:def 3; :: thesis: verum

set n = len x1;

A1: x2 is FinSequence of COMPLEX by Lm2;

x1 is FinSequence of COMPLEX by Lm2;

then reconsider z1 = x1 as Element of (len x1) -tuples_on COMPLEX by FINSEQ_2:92;

assume len x1 = len x2 ; :: thesis: len (x1 + x2) = len x1

then reconsider z2 = x2 as Element of (len x1) -tuples_on COMPLEX by A1, FINSEQ_2:92;

dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124;

hence len (x1 + x2) = len x1 by FINSEQ_1:def 3; :: thesis: verum