let F be FinSequence of REAL ; :: thesis: ( F + (- F) = 0* (len F) & F - F = 0* (len F) )
set n = len F;
reconsider R = F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: R + (- R) = (len F) |-> 0 by RVSUM_1:22;
hence F + (- F) = 0* (len F) by EUCLID:def 4; :: thesis: F - F = 0* (len F)
thus F - F = 0* (len F) by A1, EUCLID:def 4; :: thesis: verum