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:110;
((len F) |-> 0 ) - R = - R by RVSUM_1:54;
hence (0* (len F)) - F = - F by EUCLID:def 4; :: thesis: verum