let F1, F2 be FinSequence of REAL ; :: thesis: ( len F1 = len F2 implies F1 = (F1 + F2) - F2 )
assume A1: len F1 = len F2 ; :: thesis: F1 = (F1 + F2) - F2
set n = len F1;
reconsider R1 = F1, R2 = F2 as Element of (len F1) -tuples_on REAL by A1, FINSEQ_2:110;
R1 = (R1 + R2) - R2 by RVSUM_1:63;
hence F1 = (F1 + F2) - F2 ; :: thesis: verum