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