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