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