let D be non empty set ; :: thesis: for d being Element of D
for k being natural Number holds k |-> d is FinSequence of D
let d be Element of D; :: thesis: for k being natural Number holds k |-> d is FinSequence of D
let k be natural Number ; :: thesis: k |-> d is FinSequence of D
set s = k |-> d;
rng (k |-> d) c= {d} by FUNCOP_1:13;
then rng (k |-> d) c= D by XBOOLE_1:1;
hence k |-> d is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum