theorem Th42: :: FINSEQ_6:42

for D being non empty set
for f being FinSequence of D st f <> {} holds
f /. 1 in rng f