a + b >= 0 + b by XREAL_1:6;
then ( b >= 1 & b <= a + b ) by NAT_1:14;
then b in Seg (a + b) ;
hence ((a + b) |-> x) . b = x by FINSEQ_2:57; :: thesis: verum