f . (1 + 0) < f . 0 by SEQM_3:def 7;
hence difference f is negative by XREAL_1:49; :: thesis: verum