let k be Nat; :: thesis: for a being set holds k --> a is XFinSequence
let a be set ; :: thesis: k --> a is XFinSequence
reconsider p = k --> a as Function ;
( k in NAT & dom p = k ) by FUNCOP_1:13, ORDINAL1:def 12;
hence k --> a is XFinSequence by Th7; :: thesis: verum