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