dom (f + a) = len f by VALUED_1:def 2;
then B5: f + a is XFinSequence by AFINSQ_1:7;
rng (f + a) c= REAL by VALUED_0:def 3;
hence a + f is XFinSequence of by B5, RELAT_1:def 19; :: thesis: verum