let k be Nat; :: thesis: for a being set holds (Seg k) --> a is FinSequence
let a be set ; :: thesis: (Seg k) --> a is FinSequence
set p = (Seg k) --> a;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
dom ((Seg k) --> a) = Seg k by FUNCOP_1:13;
hence (Seg k) --> a is FinSequence by FINSEQ_1:def 2; :: thesis: verum