theorem :: FINSEQ_3:32

for p being FinSequence st rng p <> {} holds
1 in dom p