let x1, x2 be real-valued FinSequence; :: thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 )
set n = len x1;
A1: x2 is FinSequence of REAL by Lm2;
x1 is FinSequence of REAL by Lm2;
then reconsider z1 = x1 as Element of (len x1) -tuples_on REAL 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 REAL 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