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