theorem :: FIB_NUM2:13

for p being FinSubsequence holds rng (Seq p) c= rng p by RELAT_1:26;