let i be Nat; :: thesis: for x being object st i > 0 holds
{[i,x]} is FinSubsequence
let x be object ; :: thesis: ( i > 0 implies {[i,x]} is FinSubsequence )
assume A1: i > 0 ; :: thesis: {[i,x]} is FinSubsequence
A2: dom {[i,x]} = {i} by RELAT_1:9;
{i} c= Seg i
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {i} or x in Seg i )
assume x in {i} ; :: thesis: x in Seg i
then x = i by TARSKI:def 1;
hence x in Seg i by A1, Th3; :: thesis: verum
end;
hence {[i,x]} is FinSubsequence by A2, Def12; :: thesis: verum