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