( 1 <= k & k + 0 <= k + l ) by NAT_1:14, XREAL_1:6;
then ( 1 <= k & k <= len f ) by CARD_1:def 7;
then k in dom f by FINSEQ_3:25;
hence ((len f) |-> a) . k = a by Lmkdf; :: thesis: verum