let i be Integer; :: thesis: for f being FinSequence st 1 <= i & i <= len f holds

i in dom f

let f be FinSequence; :: thesis: ( 1 <= i & i <= len f implies i in dom f )

assume that

A1: 1 <= i and

A2: i <= len f ; :: thesis: i in dom f

i is Element of NAT by A1, INT_1:3;

hence i in dom f by A1, A2, FINSEQ_3:25; :: thesis: verum

i in dom f

let f be FinSequence; :: thesis: ( 1 <= i & i <= len f implies i in dom f )

assume that

A1: 1 <= i and

A2: i <= len f ; :: thesis: i in dom f

i is Element of NAT by A1, INT_1:3;

hence i in dom f by A1, A2, FINSEQ_3:25; :: thesis: verum