take <*> REAL ; :: thesis: <*> REAL is non-increasing
let n be Nat; :: according to RFINSEQ:def 3 :: thesis: ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) )
thus ( n in dom (<*> REAL) & n + 1 in dom (<*> REAL) implies (<*> REAL) . n >= (<*> REAL) . (n + 1) ) ; :: thesis: verum