a + b > a + 0 by XREAL_1:6;
then a + b > len (a |-> x) ;
hence (a |-> x) . (a + b) is zero ; :: thesis: verum