for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds
R is non-increasing