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

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