let p be FinSequence; :: thesis: for k being Nat st k in dom p holds
for i being Nat st 1 <= i & i <= k holds
i in dom p
let k be Nat; :: thesis: ( k in dom p implies for i being Nat st 1 <= i & i <= k holds
i in dom p )
assume A1: k in dom p ; :: thesis: for i being Nat st 1 <= i & i <= k holds
i in dom p
let i be 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
k <= len p by A1, Th25;
then i <= len p by A3, XXREAL_0:2;
hence i in dom p by A2, Th25; :: thesis: verum