let p be FinSequence; :: thesis: for k being Element of NAT st k in dom p holds
for i being Element of NAT st 1 <= i & i <= k holds
i in dom p
let k be Element of NAT ; :: thesis: ( k in dom p implies for i being Element of NAT st 1 <= i & i <= k holds
i in dom p )
assume A1: k in dom p ; :: thesis: for i being Element of NAT st 1 <= i & i <= k holds
i in dom p
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= k implies i in dom p )
assume that
A2: 1 <= i and
A3: i <= k ; :: thesis: i in dom p
consider l being Nat such that
A4: dom p = Seg l by FINSEQ_1:def 2;
k <= l by A1, A4, FINSEQ_1:1;
then i <= l by A3, XXREAL_0:2;
hence i in dom p by A2, A4, FINSEQ_1:1; :: thesis: verum