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

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