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

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