A8: 1 < t + 1 by Lm1, XREAL_1:39;
dom (F_dp1 (t,a)) = Seg (len (F_dp1 (t,a))) by FINSEQ_1:def 3
.= Seg (t + 1) by Def4 ;
then 1 in dom (F_dp1 (t,a)) by A8;
hence not rng (F_dp1 (t,a)) is empty by FUNCT_1:3; :: thesis: verum