theorem :: FINSEQ_2:57

for k being natural Number
for d being object
for w being set st w in Seg k holds
(k |-> d) . w = d by FUNCOP_1:7;