theorem :: MATRIXR1:5

for F being FinSequence of REAL holds F - (0* (len F)) = F