set X = { <*0,k*> where k is Element of NAT : verum } ;
for a being object st a in { <*0,k*> where k is Element of NAT : verum } holds
a is FinSequence

proof

let a be object ; :: thesis: ( a in { <*0,k*> where k is Element of NAT : verum } implies a is FinSequence )
assume a in { <*0,k*> where k is Element of NAT : verum } ; :: thesis: a is FinSequence
then consider k being Element of NAT such that
A1: a = <*0,k*> ;
thus a is FinSequence by A1; :: thesis: verum

end;

hence { <*0,k*> where k is Element of NAT : verum } is FinSequence-membered set by FINSEQ_1:def 19; :: thesis: verum