let k be Nat; :: thesis: for a being set holds k --> a is XFinSequence
let a be set ; :: thesis: k --> a is XFinSequence
A1: k in NAT by ORDINAL1:def 13;
reconsider p = k --> a as Function ;
dom p = k by FUNCOP_1:19;
hence k --> a is XFinSequence by A1, AFINSQ_1:7; :: thesis: verum