let D be non empty set ; :: thesis: for f being FinSequence of D st f <> {} holds
f /. 1 in rng f
let f be FinSequence of D; :: thesis: ( f <> {} implies f /. 1 in rng f )
assume f <> {} ; :: thesis: f /. 1 in rng f
then 1 in dom f by FINSEQ_5:6;
hence f /. 1 in rng f by PARTFUN2:2; :: thesis: verum