let k be Nat; :: thesis: for D being non empty set
for d being Element of D holds k |-> d is FinSequence of D
let D be non empty set ; :: thesis: for d being Element of D holds k |-> d is FinSequence of D
let d be Element of D; :: 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