let k be Element of NAT ; :: thesis: for a being set st k >= 1 holds
{[k,a]} is FinSubsequence
let a be set ; :: thesis: ( k >= 1 implies {[k,a]} is FinSubsequence )
reconsider H = {[k,a]} as Function ;
A1: dom H = {k} by RELAT_1:9;
assume A2: k >= 1 ; :: thesis: {[k,a]} is FinSubsequence
dom H c= Seg k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom H or x in Seg k )
assume x in dom H ; :: thesis: x in Seg k
then x = k by A1, TARSKI:def 1;
hence x in Seg k by A2; :: thesis: verum

end;

hence {[k,a]} is FinSubsequence by FINSEQ_1:def 12; :: thesis: verum