let i, j, l be natural Number ; :: 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:5;
hence ( i in Seg l implies i in Seg (l + j) ) ; :: thesis: verum