f + (- x) is len f -element ;
hence f - x is len f -element by VALUED_1:def 3; :: thesis: verum