let n be Nat; :: thesis: for D being non empty set
for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
let D be non empty set ; :: thesis: for p being FinSequence of D st 1 <= n & n <= len p holds
p . n is Element of D
let p be FinSequence of D; :: thesis: ( 1 <= n & n <= len p implies p . n is Element of D )
assume ( 1 <= n & n <= len p ) ; :: thesis: p . n is Element of D
then n in Seg (len p) by FINSEQ_1:1;
then n in dom p by FINSEQ_1:def 3;
then A1: p . n in rng p by FUNCT_1:def 3;
rng p c= D by FINSEQ_1:def 4;
hence p . n is Element of D by A1; :: thesis: verum