let i, l, j be Nat; :: thesis: ( i in Seg l implies i in Seg (l + j) )
l <= l + j by NAT_1:11;
then Seg l c= Seg (l + j) by FINSEQ_1:7;
hence ( i in Seg l implies i in Seg (l + j) ) ; :: thesis: verum