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 A1: ( 1 <= i & i <= len f ) ; :: thesis: i in dom f
then i is Element of NAT by INT_1:16;
hence i in dom f by A1, FINSEQ_3:27; :: thesis: verum