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