f . (1 + 0) > f . 0 by SEQM_3:def 6;
hence difference f is positive by XREAL_1:50; :: thesis: verum