let X be set ; :: thesis: for p being FinSequence of X
for ii being Integer st 1 <= ii & ii <= len p holds
p . ii in X
let p be FinSequence of X; :: thesis: for ii being Integer st 1 <= ii & ii <= len p holds
p . ii in X
let ii be Integer; :: thesis: ( 1 <= ii & ii <= len p implies p . ii in X )
assume that
A1: 1 <= ii and
A2: ii <= len p ; :: thesis: p . ii in X
reconsider ii = ii as Element of NAT by A1, INT_1:3;
ii in dom p by A1, A2, FINSEQ_3:25;
hence p . ii in X by PARTFUN1:4; :: thesis: verum