let X be set ; :: thesis: for p being FinSequence of X
for ii being Integer st 1 <= ii & ii <= len p holds
p /. ii = p . ii
let p be FinSequence of X; :: thesis: for ii being Integer st 1 <= ii & ii <= len p holds
p /. ii = p . ii
let ii be Integer; :: thesis: ( 1 <= ii & ii <= len p implies p /. ii = p . ii )
assume A1: ( 1 <= ii & ii <= len p ) ; :: thesis: p /. ii = p . ii
then reconsider ii = ii as Element of NAT by INT_1:16;
ii in dom p by A1, FINSEQ_3:27;
hence p /. ii = p . ii by PARTFUN1:def 8; :: thesis: verum