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 that

A1: 1 <= ii and

A2: ii <= len p ; :: thesis: p /. ii = p . ii

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 = p . ii by PARTFUN1:def 6; :: thesis: verum

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 that

A1: 1 <= ii and

A2: ii <= len p ; :: thesis: p /. ii = p . ii

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 = p . ii by PARTFUN1:def 6; :: thesis: verum