theorem Lmkdf: :: FINSEQ_9:20

for a being Complex
for f being FinSequence
for k being Nat st k in dom f holds
((len f) |-> a) . k = a